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

Autor/en:
Alexander Steen
Umfang:
244
EAN/ISBN:
978-3-89838-739-2
Erscheinungsdatum:
Freitag, 14. September 2018
Band:
345
Ausgabe:
Softcover
Buchreihe:
Dissertations in Artificial Intelligence
Kategorien:
Buch
Künstliche Intelligenz
Dissertations in Artificial Intelligence
Verfügbarkeit: lieferbar
Preis:
inkl. 7% MWSt
60,00 €
Automated theorem proving systems validate or refute the statement that a conjecture is a logical consequence of a given set of assumptions. These systems can be used 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 yields effective means for reasoning within expressive non-classical logics, e.g. enabling the formal analysis of philosophical arguments from metaphysics.

In this thesis the theoretical foundations and the practical components for implementing the effective automated theorem proving system Leo-III for higher-order logic are presented. Leo-III is based on an extensional paramodulation calculus and implements additional practically motivated inference rules including equational simplification routines such as heuristic rewriting and support for reasoning with choice. The system encompasses a flexible mechanism for asynchronous cooperation with first-order reasoning systems, a powerful proof search procedure and a sophisticated and efficient set of underlying data structures. Pragmatic and practically significant features of Leo-III are discussed, including its native support for polymorphic higher-order logic and reasoning in higher-order quantified modal logics.