Advances in Equational Theorem Proving - Architecture, Algorithms, and Redundancy Avoidance

Fortschritte im Gleichheitsbeweisen - Architektur, Algorithmen und Redundanzvermeidung

  • Automated theorem proving is a search problem and, by its undecidability, a very difficult one. The challenge in the development of a practically successful prover is the mapping of the extensively developed theory into a program that runs efficiently on a computer. Starting from a level-based system model for automated theorem provers, in this work we present different techniques that are important for the development of powerful equational theorem provers. The contributions can be divided into three areas: Architecture. We present a novel prover architecture that is based on a set-based compression scheme. With moderate additional computational costs we achieve a substantial reduction of the memory requirements. Further wins are architectural clarity, the easy provision of proof objects, and a new way to parallelize a prover which shows respectable speed-ups in practice. The compact representation paves the way to new applications of automated equational provers in the area of verification systems. Algorithms. To improve the speed of a prover we need efficient solutions for the most time-consuming sub-tasks. We demonstrate improvements of several orders of magnitude for two of the most widely used term orderings, LPO and KBO. Other important contributions are a novel generic unsatisfiability test for ordering constraints and, based on that, a sufficient ground reducibility criterion with an excellent cost-benefit ratio. Redundancy avoidance. The notion of redundancy is of central importance to justify simplifying inferences which are used to prune the search space. In our experience with unfailing completion, the usual notion of redundancy is not strong enough. In the presence of associativity and commutativity, the provers often get stuck enumerating equations that are permutations of each other. By extending and refining the proof ordering, many more equations can be shown redundant. Furthermore, our refinement of the unfailing completion approach allows us to use redundant equations for simplification without the need to consider them for generating inferences. We describe the efficient implementation of several redundancy criteria and experimentally investigate their influence on the proof search. The combination of these techniques results in a considerable improvement of the practical performance of a prover, which we demonstrate with extensive experiments for the automated theorem prover Waldmeister. The progress achieved allows the prover to solve problems that were previously out of reach. This considerably enhances the potential of the prover and opens up the way for new applications.
  • Automatisches Theorembeweisen ist ein spezielles Suchproblem, das aufgrund seiner Unentscheidbarkeit sehr schwierig ist. Die Herausforderung bei der Entwicklung praktisch leistungsfähiger Beweiser liegt darin, die reich entwickelte Theorie so in ein Programm abzubilden, daß dieses effizient auf dem Rechner läuft. Ausgehend von einem Schichtenmodell für automatische Theorembeweiser stellen wir in dieser Arbeit verschiedene Techniken vor, die für die Entwicklung leistungsfähiger Gleichheitsbeweiser von Bedeutung sind. Die Beiträge lassen sich in drei Gruppen einteilen. Architektur. Wir stellen eine neuartige Beweiserarchitektur vor, die eine mengenbasierte Kompressionsstrategie verfolgt. Mit wenig zusätzlichem Berechnungsaufwand läßt sich der Speicherbedarf erheblich reduzieren. Die Architektur hat eine Reihe weiterer schöner Eigenschaften. So können ohne Zusatzaufwand detaillierte Beweisobjekte ausgegeben werden. Weiterhin eröffnet sich der Weg zu einer effizienten Parallelisierung des Beweisers, die in der Praxis sehr gute Ergebnisse zeigt. Schließlich ermöglicht die kompakte Darstellung neue Anwendungen für automatische Gleichheitsbeweiser im Bereich von Verifikationssystemen. Algorithmen. Um die Geschwindigkeit eines Beweisers zu steigern, gilt es, effiziente Lösungen für die Routinen zu finden, die den Hauptteil der Rechenzeit benötigen. Wir zeigen Beschleunigungen von mehreren Größenordnungen für zwei der am meisten verwendeten Termordnungen, LPO und KBO. Besonders hervorzuheben sind ein neuer generischer Unerfüllbarkeitstest für Ordnungsconstraints, der polynomialen Laufzeitbedarf hat, und darauf aufbauend ein hinreichender Grundreduzierbarkeitstest mit einem hervorragenden Kosten-Nutzen-Verhältnis. Redundanzvermeidung. Auf Kalkülebene ist der Begriff der Redundanz zentral für die Rechtfertigung simplifizierender Inferenzen. Deren Verwendung hat eine wesentliche Beschränkung des Suchraumes zur Folge. In unserer praktischen Erfahrung ist der Redundanzbegriff der Vervollständigung ohne Abbruch zu schwach. Bei Vorliegen von Assoziativität und Kommutativität werden sehr viele ähnliche Gleichungen erzeugt. Durch Erweiterung und Verfeinerung der Beweisordnung können deutlich mehr Gleichungen als redundant nachgewiesen werden. Außerdem erlaubt der verfeinerte Kalkül, redundante Gleichungen zur Simplifikation zu verwenden, ohne sie für generierende Inferenzen berücksichtigen zu müssen. Wir beschreiben die effiziente Implementierung einiger Redundanzkriterien und untersuchen experimentell ihren Einfluß auf die Beweissuche. Die Kombination der beschriebenen Techniken führt zu einer erheblichen Steigerung der Leistungsfähigkeit eines Beweisers, wie wir anhand des automatischen Beweisers Waldmeister in ausführlichen Experimenten demonstrieren. Diese Fortschritte erlauben das Lösen von Problemen, die vorher jenseits der Möglichkeiten des Beweisers waren. Mit Hilfe der vorgestellten Techniken lassen sich neue Anwendungsfelder für automatische Gleichheitsbeweiser erschließen.

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Bernd Löchner
URN (permanent link):urn:nbn:de:hbz:386-kluedo-19691
Advisor:Jürgen Avenhaus
Document Type:Doctoral Thesis
Language of publication:English
Year of Completion:2005
Year of Publication:2005
Publishing Institute:Technische Universität Kaiserslautern
Granting Institute:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2005/07/20
Tag:Knuth-Bendix-Vervollständigung; Redundanzvermeidung; Software-Architektur
Knuth-Bendix completion; automated theorem proving; implementation
GND-Keyword:Algorithmus; Automatisches Beweisverfahren ; Effizienter Algorithmus ; Implementierung
Faculties / Organisational entities:Fachbereich Informatik
CCS-Classification (computer science):F.4.1 Mathematical Logic (F.1.1, I.2.2-4)
DDC-Cassification:004 Datenverarbeitung; Informatik

$Rev: 12793 $