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

Share
Author
Steen, A.
Pub. date
October 2018
Pages
246
Binding
softcover
Volume
345 of Dissertations in Artificial Intelligence
ISBN print
978-1-61499-919-5
Subject
Artificial Intelligence, Computer Science
€60 / US$74 / £54 Excl. VAT
Order Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III ISBN @ €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.