Logo des Repositoriums
 
Zeitschriftenartikel

Extensional Paramodulation for Higher-Order Logic and Its Effective Implementation Leo-III

Vorschaubild nicht verfügbar

Volltext URI

Dokumententyp

Text/Journal Article

Zusatzinformation

Datum

2020

Zeitschriftentitel

ISSN der Zeitschrift

Bandtitel

Verlag

Springer

Zusammenfassung

Automation of classical higher-order logic faces various theoretical and practical challenges. On a theoretical level, powerful calculi for effective equality reasoning from first-order theorem proving cannot be lifted to the higher-order domain in a simple manner. Practically, implementations of higher-order reasoning systems have to incorporate procedures that often have high time complexity or are not decidable in general. In my dissertation, both the theoretical and the practical challenges of designing an effective higher-order reasoning system are studied. The resulting system, the automated theorem prover Leo-III, is one of the most effective and versatile systems, in terms of supported logical formalisms, to date.

Beschreibung

Steen, Alexander (2020): Extensional Paramodulation for Higher-Order Logic and Its Effective Implementation Leo-III. KI - Künstliche Intelligenz: Vol. 34, No. 1. DOI: 10.1007/s13218-019-00628-8. Springer. PISSN: 1610-1987. pp. 105-108

Zitierform

Tags