TPTP World Infrastructure for Non-classical Logics

• URL: http://arxiv.org/abs/2508.09318v1
• Date: Tue, 12 Aug 2025 20:05:52 GMT
• Title: TPTP World Infrastructure for Non-classical Logics
• Authors: Alexander Steen, Geoff Sutcliffe,
• Abstract summary: The TPTP World supports research, development, and deployment of Automated Theorem Proving (ATP) systems.<n>This paper provides a self-contained overview of the TPTP World infrastructure for ATP in non-classical logics.
• Score: 51.61531917413708
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The TPTP World is the well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. The TPTP World supports a range of classical logics, and since release v9.0.0 has supported non-classical logics. This paper provides a self-contained comprehensive overview of the TPTP World infrastructure for ATP in non-classical logics: the non-classical language extension, problems and solutions, and tool support. A detailed description of use of the infrastructure for quantified normal multi-modal logic is given.

Related papers

• Faithful Logic Embeddings in HOL -- Deep and Shallow [0.0]
  This paper presents a method for the simultaneous deployment of deep and shallow embeddings of various degrees in classical higher-order logic.<n>The method is beneficial for logic education, research and application and is illustrated here using a simple propositional modal logic.
  arXiv  Detail & Related papers  (2025-02-26T17:08:07Z)
• Proceedings Modalities in substructural logics: Applications at the interfaces of logic, language and computation [0.0]
  The focus of the workshop is on applications in the areas of interest to the ESSLLI community, in particular logical approaches to natural language syntax and semantics and the dynamics of reasoning. The workshop is held with the support of the Horizon 2020 MSCA-Rise project MOSAIC.
  arXiv  Detail & Related papers  (2023-08-01T22:40:19Z)
• Solving Quantified Modal Logic Problems by Translation to Classical Logics [47.24825031148412]
  The problems are translated to both typed first-order and higher-order logic using an embedding approach. The results from native modal logic ATP systems are considered, and compared with the results from the embedding approach.
  arXiv  Detail & Related papers  (2022-12-19T16:02:14Z)
• Bridging between LegalRuleML and TPTP for Automated Normative Reasoning (extended version) [77.34726150561087]
  LegalRuleML is an XML-based representation framework for modeling and exchanging normative rules. The TPTP input and output formats are general-purpose standards for the interaction with automated reasoning systems. We provide a bridge between the two communities by defining a logic-pluralistic normative reasoning language based on the TPTP format.
  arXiv  Detail & Related papers  (2022-09-12T08:42:34Z)
• Discourse-Aware Graph Networks for Textual Logical Reasoning [142.0097357999134]
  Passage-level logical relations represent entailment or contradiction between propositional units (e.g., a concluding sentence) We propose logic structural-constraint modeling to solve the logical reasoning QA and introduce discourse-aware graph networks (DAGNs) The networks first construct logic graphs leveraging in-line discourse connectives and generic logic theories, then learn logic representations by end-to-end evolving the logic relations with an edge-reasoning mechanism and updating the graph features.
  arXiv  Detail & Related papers  (2022-07-04T14:38:49Z)
• An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning [91.3755431537592]
  The logic embedding tool provides a procedural encoding for non-classical reasoning problems into classical higher-order logic. It can support an increasing number of different non-classical logics as reasoning targets.
  arXiv  Detail & Related papers  (2022-03-23T12:08:51Z)
• Automated Reasoning in Non-classical Logics in the TPTP World [58.720142291102135]
  The TPTP World currently supports only classical logics. Similar standards for non-classical logic reasoning do not exist. This paper describes the latest extension of the TPTP World, which provides languages and infrastructure for reasoning in non-classical logics.
  arXiv  Detail & Related papers  (2022-02-20T15:29:30Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.