Seit den 1980er Jahren ist das Forschungsinteresse am Feld des automatisierten Fahrens schnell gewachsen und wächst auch heute noch exponentiell weiter. Damit einhergehend sind zahlreiche neue Ansätze, Techniken und Lösungen entstanden. Trotzdem ist weitere Forschungsarbeit erforderlich, um die Vision des automatisierten Fahrens in allen denkbaren Szenarien verwirklichen zu können. Insbesondere urbane Szenarien stellen in Bezug auf automatisiertes Fahren nach wie vor eine komplexe wissenschaftliche Herausforderung dar.

Die vorliegende Arbeit beschäftigt sich mit der Entwicklung eines Szenariointerpretationskonzeptes für automatisiertes Fahren an urbanen Kreuzungen. Der Fokus liegt dabei auf der Interpretation der zur Verfügung stehenden Daten des Unfallwahrnehmungsmoduls, mit dem Ziel, das Ego-Fahrzeug ein gewünschtes Fahrmanöver ausführen zu lassen.

Der erste Beitrag dieser Arbeit behandelt die Problemadressierung und -analyse und nimmt eine Klassifikation aller möglichen Szenarien in Bezug auf potentielle Konflikte mit anderen Verkehrsteilnehmern vor. Diese Klassifikation veranschaulicht den Bedarf nach einer Lösung zur Interpretation solcher Szenarien und Umsetzung entsprechender Fahrmanöver. Der entwickelte Lösungsansatz basiert auf der Berechnung einer diskreten Wahrscheinlichkeitsverteilung, welche die verschiedenen Zustände der Passierbarkeit von Kreuzungen unter Berücksichtigung aller möglichen Ampelschaltungen und Verkehrsszenen für Ego-Fahrzeuge abbildet. Das vorliegende Konzept beachtet dabei sowohl Input-Unsicherheiten als auch Schwankungen über die Zeit.

Die Beiträge dieser Arbeit stützen sich auf das Kernkonzept der elementaren Situationen. Die Idee dahinter ist das Zerlegen eines gewünschten Fahrmanövers in einzelne Sequenzen. Diese Vereinfachung ermöglicht eine Einschätzung der potentiellen Bewegungen anderer Verkehrsteilnehmer aus denen anschließend die Belegwahrscheinlichkeiten für die einzelnen elementaren Situationen berechnet werden können.

Ein weiterer relevanter Beitrag beschreibt die Entwicklung einer taktischen Manöverplanung, welche nicht sichtbare Bereiche, beziehungsweise fehlende Informationen innerhalb von Kreuzungen zum Gegenstand hat.

Die prototypische Umsetzung der Ansätze ermöglicht die Erfassung der Ergebnisse als proof of concept mit realen Daten. Weiterhin kann anhand der erzielten Ergebnisse angenommen werden, dass die entwickelte Lösung für die Szenariointerpretationen an urbanen Kreuzungen geeignet ist.

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.