Extensional Higher-Order Paramodulation in Leo-III.
Saved in:
| Title: | Extensional Higher-Order Paramodulation in Leo-III. |
|---|---|
| Authors: | Steen, Alexander1 alexander.steen@uni.lu, Benzmüller, Christoph1,2 |
| Source: | Journal of Automated Reasoning. Aug2021, Vol. 65 Issue 6, p775-807. 33p. |
| Subjects: | Deontic logic, Automatic theorem proving, Proof theory, Source code, Boolean functions |
| 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 many quantified normal 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. [ABSTRACT FROM AUTHOR] |
| Copyright of Journal of Automated Reasoning is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
| FullText | Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 151066805 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Extensional Higher-Order Paramodulation in Leo-III. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Steen%2C+Alexander%22">Steen, Alexander</searchLink><relatesTo>1</relatesTo><i> alexander.steen@uni.lu</i><br /><searchLink fieldCode="AR" term="%22Benzmüller%2C+Christoph%22">Benzmüller, Christoph</searchLink><relatesTo>1,2</relatesTo> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Journal+of+Automated+Reasoning%22">Journal of Automated Reasoning</searchLink>. Aug2021, Vol. 65 Issue 6, p775-807. 33p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Deontic+logic%22">Deontic logic</searchLink><br /><searchLink fieldCode="DE" term="%22Automatic+theorem+proving%22">Automatic theorem proving</searchLink><br /><searchLink fieldCode="DE" term="%22Proof+theory%22">Proof theory</searchLink><br /><searchLink fieldCode="DE" term="%22Source+code%22">Source code</searchLink><br /><searchLink fieldCode="DE" term="%22Boolean+functions%22">Boolean functions</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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 many quantified normal 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. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Journal of Automated Reasoning is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=151066805 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1007/s10817-021-09588-x Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 33 StartPage: 775 Subjects: – SubjectFull: Deontic logic Type: general – SubjectFull: Automatic theorem proving Type: general – SubjectFull: Proof theory Type: general – SubjectFull: Source code Type: general – SubjectFull: Boolean functions Type: general Titles: – TitleFull: Extensional Higher-Order Paramodulation in Leo-III. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Steen, Alexander – PersonEntity: Name: NameFull: Benzmüller, Christoph IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 08 Text: Aug2021 Type: published Y: 2021 Identifiers: – Type: issn-print Value: 01687433 Numbering: – Type: volume Value: 65 – Type: issue Value: 6 Titles: – TitleFull: Journal of Automated Reasoning Type: main |
| ResultId | 1 |
