Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III
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.