Logo des Repositoriums
 
Zeitschriftenartikel

Higher-order theorem proving and its applications

Vorschaubild nicht verfügbar

Volltext URI

Dokumententyp

Text/Journal Article

Zusatzinformation

Datum

2019

Zeitschriftentitel

ISSN der Zeitschrift

Bandtitel

Verlag

De Gruyter

Zusammenfassung

Automated theorem proving systems validate or refute whether a conjecture is a logical consequence of a given set of assumptions. Higher-order provers have been successfully applied in academic and industrial applications, such as planning, software and hardware verification, or knowledge-based systems. Recent studies moreover suggest that automation of higher-order logic, in particular, yields effective means for reasoning within expressive non-classical logics, enabling a whole new range of applications, including computer-assisted formal analysis of arguments in metaphysics. My work focuses on the theoretical foundations, effective implementation and practical application of higher-order theorem proving systems. This article briefly introduces higher-order reasoning in general and presents an overview of the design and implementation of the higher-order theorem prover Leo-III. In the second part, some example applications of Leo-III are discussed.

Beschreibung

Steen, Alexander (2019): Higher-order theorem proving and its applications. it - Information Technology: Vol. 61, No. 4. DOI: 10.1515/itit-2019-0001. Berlin: De Gruyter. PISSN: 2196-7032. pp. 187-191

Zitierform

Tags