In der vorliegenden Dissertation werden sowohl die theoretischen Grundlagen als auch Implementierungstechniken für die Entwicklung eines effektiven automatischen Theorembeweisers für Prädikatenlogik höherer Stufe präsentiert. Ein Hauptaugenmerk der Arbeit liegt dabei auf der Demonstration der Machbarkeit, ein performantes Theorembeweisersystem für das automatische Schließen in gleichheitsbasierter extensionaler Typentheorie (hier gleichbedeutend mit Prädikatenlogik höherer Stufe) mit Hilfe eines Paramodulationskalküls zu implementieren. Zu diesem Zweck wird ein korrekter und vollständiger Paramodulationskalkül für extensionale Typentheorie unter Henkinsemantik erarbeitet. Für den Vollständigkeitsbeweis wurden bereits existierende Beweistechniken der abstrakten Konsistenz vereinheitlicht und, für den hier präsentierten gleichheitsbasierten Ansatz, vereinfacht.

Der praktisch motivierte Hauptteil der Arbeit diskutiert die Softwarearchitektur und Implementierung des neuen, auf dem zuvor entwickelten Paramodulationskalkül basierten, Theorembeweiser Leo-III. Dabei implementiert Leo-III eine um weitgehend praktische Aspekte erweiterte Version des Kalküls und umfasst z.B. gleichheitsbasierte Simplifikationtechniken, heuristische Termersetzung und Unterstützung für das Schließen mit Auswahlfunktionen. Leo-III umfasst als Deduktionsplattform zudem ein flexibles, asynchrones Kommunikationssystem für die Kooperation mit externen Systemen, insbesondere mit Theorembeweisern für Prädikatenlogik erster Stufe. Das System implementiert fortschrittliche Beweissuchemethoden und basiert diese auf effizienten Datenstrukturen. Außerdem werden weitere, praktisch relevante Anwendungen und Fähigkeiten von Leo-III skizziert, darunter die Unterstützung von polymorpher Typentheorie und das Schließen in allen normalen quantifizierten Modallogiken. Die Effektivität von Leo-III wird durch eine breite Evaluation auf verschiedenen Datensätzen untersucht. Die Ergebnisse dieser Evaluation bestätigen dass Leo-III zu den aktuell stärksten Theorembeweisern für höherstufige Prädikatenlogik zählt und zudem für ein breites Spektrum von Anwendungen nutzbar ist.

----------------------------------------------------------------------------------------------------------

In this thesis the theoretical foundations and the practical components for implementing an effective automated theorem proving system for higher-order logic are presented. A primary focus of this thesis is the provision of evidence that a paramodulation-based proof calculus can effectively be employed for performant equational reasoning in Extensional Type Theory (higher-order logic). To that end, a sound and complete paramodulation calculus for extensional higher-order logic with Henkin semantics is presented. The completeness proof hereby unifies and simplifies existing abstract consistency techniques for a formulation of higher-order logic that is based on primitive equality as sole logical connective.
In the practically motivated main part of this thesis, the design and architecture of the new higher-order theorem prover Leo-III is presented. Leo-III is based on the above 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. An evaluation on a heterogeneous set of benchmark problems confirms that Leo-III is one of the most effective and versatile higher-order automated reasoning systems to date.