Unification in higher-order resolution

Abstract

Die Methoden der Beweisanalyse und die in ihrem Kontext entwickelten logischen Kalküle wurden ursprünglich zur Erlangung theoretischer Ergebnisse herangezogen. Die zunehmende Rechenkapazität von Computern erlaubt jedoch inzwischen auch die praktische Anwendung dieser Methoden zur Beweissuche.<br />Einer der zentralen Fortschritte war Robinsons Einführung des Resolutionskalküls, der sich speziell zur automatisierten Beweissuche eignet.<br />Gerade im ursprünglichen Anwendungsgebiet der Prädikatenlogik erster Stufe besitzt es eine verhältnismäßig niedrige Suchkomplexität.<br />Unifikation, das Kernstück des Resolutionskalküls, ist hier effizient entscheidbar und unitär, d.h. es gibt nur höchstens einen allgemeinsten Unifikator.<br />Zum Formalisieren von mathematischen Beweisen sind die Prädikatenlogiken höherer Stufe wesentlich besser geeignet als diejenige erster Stufe.<br />In diesem Fall ist die Unifikation jedoch nur mehr semi-entscheidbar:<br />die Menge der allgemeinsten (Prä-)Unifikatoren ist von abzählbar unendlicher Kardinalität, die Suche nach einem Unifikator terminiert im Allgemeinen auch nicht.<br />Wissenschaftlich behandelt wurden bisher hauptsächlich der allgemeine Fall und syntaktische Einschränkungen wie Anzahl und Typ der vorkommenden Variablen oder die Termintiefe, mit dem Ziel das Teilproblem entscheidbar zu machen. Das Zusammenspiel von Unifikation und Resolution erfordert noch eine gesonderte Betrachtung, da die Unifikation etwa oft aufgeschoben werden muss, eine möglichst frühe Elimination von nicht unifizierbaren Termen aber von Vorteil ist.<br />Thema der Dissertation ist, die verfeinerten Unifikationsalgorithmen für die Anwendung in der Resolution praktikabel zu machen.<br />Sie behandelt die Nachteile der aktuellen Algorithmen und stellt sie den hier entwickelten Verbesserungen gegenüber.<br />Ein besonderes Augenmerk wird dabei auf die unterschiedlichen Suchstrategien gelegt. Die Gegenüberstellung findet anhand einer Reihe von Testfällen statt und zeigt exemplarisch die Effizienz der neuen Algorithmen, was speziell im Fall der Theorie der Arithmetik zweiter Ordnung gelingt.<br />

The mathematical analysis of proofs and the creation of modern proof calculi were originally aiming more at analyzing the properties of existing proofs and less at the creation and discovery of new proofs.<br />This has changed with the introduction of computers. The advances in computer technology which resulted in increasing computing power made it more practical to search for new proofs as well. This process has culminated with the invention of the resolution calculus, a logical calculus which is extremely suitable for mechanical processing.<br />The resolution calculus was first introduced for first-order logic, in which the calculus enjoys many advantages and the search complexity is relatively small.<br />Since the resolution calculus is based on the unification principle, one of the main advantages is the fact that the first-order unification problem is decidable and unitary.<br />When lifting the calculus to higher-order logic, in which the formalizing of mathematical problems is more natural, several issues arise which render the calculus less useful in practice. The foremost of these issues is the complexity of the higher-order unification problem, which is now both infinitary and undecidable.<br />The majority of the higher-order resolution calculi and their implementations are based on either an unrestricted higher-order unification or on strongly restricted higher-order unification in which the size of the generated unifiers is restricted. The existence of more refined higher-order unification algorithms does not translate directly into more efficient resolution calculi as these algorithms are normally not well suited for automated deduction.<br />The main aim of this thesis is to bridge the gap between the practicability of the higher-order resolution calculus and the efficiency of the more refined unification algorithms.<br />The weakness of these unification algorithms with regard to automated deduction is investigated and more suitable algorithms are defined. On the other hand, the search strategies in the resolution calculi are modified in order to better suit the unification algorithms.<br />The obtained resolution calculi are compared with existing ones using a set of test cases. The conclusion drawn from this comparison is that there is a real advantage in considering the calculi introduced in this thesis when considering various classes of problems and in particular, second-order arithmetical problems.