Automated Reasoning in Non-classical Logics in the TPTP World
Non-classical logics are used in a wide spectrum of disciplines, including artificial intelligence, computer science, mathematics, and philosophy. The de-facto standard infrastructure for automated theorem proving, the TPTP World, currently supports only classical logics. Similar standards for non-classical logic reasoning do not exist (yet). This hampers practical development of reasoning systems, and limits their interoperability and application. This paper describes the latest extension of the TPTP World, which provides languages and infrastructure for reasoning in non-classical logics. The extensions integrate seamlessly with the existing TPTP World.
Code (0)
등록된 구현이 없습니다.
Tasks
Automated Theorem ProvingPhilosophySimilar Papers 제목 키워드 기반
TPTP World Infrastructure for Non-classical Logics
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…
Automated Theorem ProvingExtensional Higher-Order Paramodulation in Leo-III
Leo-III is an automated theorem prover for extensional type theory with Henkin semantics and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based proof search to higher-order logic. The p…
Bridging between LegalRuleML and TPTP for Automated Normative Reasoning (extended version)
LegalRuleML is a comprehensive XML-based representation framework for modeling and exchanging normative rules. The TPTP input and output formats, on the other hand, are general-purpose standards for the interaction with …
TranslationSolving Quantified Modal Logic Problems by Translation to Classical Logics
This article describes an evaluation of Automated Theorem Proving (ATP) systems on problems taken from the QMLTP library of first-order modal logic problems. Principally, the problems are translated to both typed first-o…
Automated Theorem ProvingTranslationThe Higher-Order Prover Leo-III (Extended Version)
The automated theorem prover Leo-III for classical higher-order logic with Henkin semantics and choice is presented. Leo-III is based on extensional higher-order paramodulation and accepts every common TPTP dialect (FOF,…