Equality Reasoning Based on Graphs

Abstract

The theoretical and practical problems of equality reasoning in Automated Deduction are notorious. A new method is presented to cope with the enormous search space that usually arises when equational axioms are present. Starting from an empty graph a production system constructs graphs which represent solutions for simpler problems defined by abstraction. These graphs contain global information and are plans for guiding the search for a proof of the original problem, represented in the final graph. The construction of equality graphs is based on the idea to reduce the differences between two terms by separating toplevel symbol and subterms of a functional term. The impact of the explicit representation of information contained in the inference system on the control of inferences is discussed in this work and the method is compared to other equality reasoning methods. The basic principle of our method is formalized and soundness and completeness results are given. An implementation of the method confirmed its adequacy for equality reasoning. Such implementations led to the rejection of previous approaches, but conducted the ideas to the development of our final inference system.

Die Behandlung der Gleichheitsrelation in automatischen Deduktionssystemen führt im allgemeinen zu erheblichen praktischen und theoretischen Problemen. In dieser Arbeit wird eine neue Methode vorgestellt, um die riesigen Suchräume zu bewältigen, die entstehen, wenn die Gleichheitsrelation in der Formelmenge vorkommt. Ausgehend von einem leeren Graphen werden mit einem Produktionsregelsystem Graphen konstruiert, welche Lösungen für einfachere, durch Abstraktion gewonnene Probleme repräsentieren. Diese Graphen enthalten globale Information und dienen als Plan um die Suche nach einem Beweis für das eigentliche Problem zu steuern. Die Konstruktion der Graphen basiert auf dem Prinzip, die Unterschiede zwischen zwei Termen durch separate Behandlung von Funktionssymbol und Untertermen zu reduzieren. In dieser Arbeit werden auch die Konsequenzen diskutiert, die sich aus der expliziten Darstellung von Information im Ableitungssystem auf die Kontrolle des Schließens ergeben. Die neue Methode wird mit anderen Methoden zur Gleichheitsbehandlung verglichen. Das grundlegende Verfahren wird formalisiert und Korrektheits- und Vollständigkeitsresultate werden geliefert. Die prinzipielle Eignung der neuen Methode zur automatischen Behandlung der Gleichheitsrelation wurde durch Implementierungen bestätigt. Solche Implementierungen führten zunächst zum Verwerfen früherer Ansätze und leiteten die Ideen, die zur Entwicklung der neuen Methode führten.