1. Extensional Higher-Order Paramodulation in Leo-III
- Author
-
Alexander Steen, Christoph Benzmüller, Deutsche Forschungsgemeinschaft [sponsor], and Volkswagenstiftung [sponsor]
- Subjects
Computer Science - Symbolic Computation ,FOS: Computer and information sciences ,03B35, 03B15, 03B45, 68T15, 68T27, 68T30, 03Bxx ,Computer Science - Logic in Computer Science ,Higher-Order Logic ,Automated Reasoning ,Computer Science - Artificial Intelligence ,Computer science ,HOL ,Automated Theorem Proving ,Symbolic Computation (cs.SC) ,Gas meter prover ,Mathematical proof ,computer.software_genre ,Higher-order logic ,Artificial Intelligence ,FOS: Mathematics ,Automated reasoning ,Computer science [C05] [Engineering, computing & technology] ,I.2.3 ,I.2.4 ,Programming language ,Deontic logic ,F.4.1 ,Mathematics - Logic ,Sciences informatiques [C05] [Ingénierie, informatique & technologie] ,Logic in Computer Science (cs.LO) ,Automated theorem proving ,Artificial Intelligence (cs.AI) ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,Type theory ,Computational Theory and Mathematics ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,Logic (math.LO) ,computer ,Software - Abstract
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 prover may cooperate with multiple external specialist reasoning systems such as first-order provers and SMT solvers. Leo-III is compatible with the TPTP/TSTP framework for input formats, reporting results and proofs, and standardized communication between reasoning systems, enabling e.g. proof reconstruction from within proof assistants such as Isabelle/HOL. Leo-III supports reasoning in polymorphic first-order and higher-order logic, in all normal quantified modal logics, as well as in different deontic logics. Its development had initiated the ongoing extension of the TPTP infrastructure to reasoning within non-classical logics., Comment: 34 pages, 7 Figures, 1 Table; submitted article
- Published
- 2021
- Full Text
- View/download PDF