Advances in equational theorem proving [Elektronische Ressource] : architecture, algorithms, and redundancy avoidance / von Bernd Löchner

Sujets

• Informatik
• Mathematics

Informations

• Publié par: technische_universitat_kaiserslautern
• Publié le: 01 janvier 2006
• Nombre de lectures: 7
• Langue: Deutsch
• Poids de l'ouvrage: 2 Mo

Extrait

Advances in
Equational Theorem Proving
{
Architecture, Algorithms, and
Redundancy Avoidance
Vom Fachbereich Informatik
der Technischen Universit˜ at Kaiserslautern
zur Verleihung des akademischen Grades
Doktor der Naturwissenschaften (Dr. rer. nat.)
genehmigte Dissertation
von
Dipl.-Inform. Bernd L˜ ochner
Datum der wissenschaftlichen Aussprache: 20. Juli 2005
Dekan: Prof. Dr. Reinhard Gotzhein
Prufungsk˜ ommision:
Vorsitzender: Prof. Dr. Arnd Poetzsch-Hefiter
Berichterstatter: Prof. Dr. Jurgen˜ Avenhaus
Prof. Dr. Klaus E. Madlener
D 386Beflehl Du Deine Wege und was Dein Herze kr˜ ankt,
der allertreusten P ege des, der den Himmel lenkt.
Der Wolken, Luft und Winden gibt Wege, Lauf und Bahn,
der wird auch Wege flnden, da Dein Fu… gehen kann.
Ihn, ihn la… tun und walten, er ist ein weiser Furst˜
und wird sich so verhalten, da… Du Dich wundern wirst,
wenn er, wie ihm gebuhret,˜ mit wunderbarem Rat
das Werk hinausgefuhret,˜ das Dich bekummert˜ hat.
Paul GerhardZusammenfassung
Automatisches Theorembeweisen ist ein spezielles Suchproblem, das aufgrund seiner
Unentscheidbarkeit sehr schwierig ist. Die Herausforderung bei der Entwicklung prak-
tisch leistungsf˜ ahiger Beweiser liegt darin, die reich entwickelte Theorie so in ein Pro-
gramm abzubilden, da… dieses e–zient auf dem Rechner l˜auft. Ausgehend von einem
Schichtenmodell fur˜ automatische Theorembeweiser stellen wir in dieser Arbeit ver-
schiedene Techniken vor, die fur˜ die Entwicklung leistungsf˜ ahiger Gleichheitsbeweiser
von Bedeutung sind. Die Beitr˜ age lassen sich in drei Gruppen einteilen.
Architektur. Wir stellen eine neuartige Beweiserarchitektur vor, die eine mengen-
basierte Kompressionsstrategie verfolgt. Mit wenig zus˜ atzlichem Berechnungsaufwand
l˜a…t sich der Speicherbedarf erheblich reduzieren. Die Architektur hat eine Reihe wei-
terer sch˜ oner Eigenschaften. So k˜ onnen ohne Zusatzaufwand detaillierte Beweisobjekte
ausgegeben werden. Weiterhin er˜ ofinet sich der Weg zu einer e–zienten Parallelisierung
des Beweisers, die in der Praxis sehr gute Ergebnisse zeigt. Schlie…lich erm˜ oglicht die
kompakte Darstellung neue Anwendungen fur˜ automatische Gleichheitsbeweiser im
Bereich von Veriflkationssystemen.
Algorithmen. Um die Geschwindigkeit eines Beweisers zu steigern, gilt es, e–ziente
L˜ osungen fur˜ die Routinen zu flnden, die den Hauptteil der Rechenzeit ben˜ otigen.
Wir zeigen Beschleunigungen von mehreren Gr˜ o…enordnungen fur˜ zwei der am meisten
verwendeten Termordnungen, LPO und KBO. Besonders hervorzuheben sind ein neuer
generischer Unerfullbark˜ eitstest fur˜ Ordnungsconstraints, der polynomialen Laufzeit-
bedarf hat, und darauf aufbauend ein hinreichender Grundreduzierbarkeitstest mit
einem hervorragenden Kosten-Nutzen-Verh˜ altnis.
Redundanzvermeidung. Auf Kalkuleb˜ ene ist der Begrifi der Redundanz zentral fur˜ die
Rechtfertigung simpliflzierender Inferenzen. Deren Verwendung hat eine wesentliche
Beschr˜ ankung des Suchraumes zur Folge. In unserer praktischen Erfahrung ist der Re-
dundanzbegrifi der Vervollst˜ andigung ohne Abbruch zu schwach. Bei Vorliegen von
Assoziativit˜ at und Kommutativit˜ at werden sehr viele ahnlic˜ he Gleichungen erzeugt.
Durch Erweiterung und Verfeinerung der Beweisordnung k˜ onnen deutlich mehr Glei-
chungen als redundant nachgewiesen werden. Au…erdem erlaubt der verfeinerte Kalkul,˜
redundante Gleichungen zur Simpliflkation zu verwenden, ohne sie fur˜ generierende In-
ferenzen beruc˜ ksichtigen zu mussen.˜ Wir beschreiben die e–ziente Implementierung
einiger Redundanzkriterien und untersuchen experimentell ihren Ein u… auf die Be-
weissuche.
Die Kombination der beschriebenen Techniken fuhrt˜ zu einer erheblichen Steigerung
der Leistungsf˜ ahigkeit eines Beweisers, wie wir anhand des automatischen Beweisers
Waldmeister in ausfuhrlic˜ hen Experimenten demonstrieren. Diese Fortschritte er-
lauben das L˜ osen von Problemen, die vorher jenseits der M˜ oglichkeiten des Beweisers
waren. Mit Hilfe der vorgestellten Techniken lassen sich neue Anwendungsfelder fur˜
automatische Gleichheitsbeweiser erschlie…en.
vviSummary
Automated theorem proving is a search problem and, by its undecidability, a very
di–cult one. The challenge in the development of a practically successful prover is the
mapping of the extensively developed theory into a program that runs e–ciently on a
computer. Starting from a level-based system model for automated theorem provers,
in this work we present difierent 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 sub-
stantial 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 veriflcation systems.
Algorithms. To improve the speed of a prover we need e–cient 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 unsatisflability test for ordering constraints
and, based on that, a su–cient ground reducibility criterion with an excellent cost-
beneflt 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 reflning the proof
ordering, many more equations can be shown redundant. Furthermore, our reflnement
of the unfailing completion approach allows us to use redundant equations for simpli-
flcation without the need to consider them for generating inferences. We describe the
e–cient implementation of several redundancy criteria and experimentally investigate
their in uence 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.
viiviiiDanksagung
Mein Dank gilt all denen, die auf vielf˜ altige Weise zum Gelingen meiner Promotion
beigetragen haben.
Herrn Prof. Dr. J. Avenhaus, der mir die M˜ oglichkeit er˜ ofinet hat, diese Arbeit zu
erstellen, danke ich fur˜ die langj˜ahrige Unterstutzung˜ und die vielen Freir˜ aume, die
˜er mir gegeben hat. Herrn Prof. Dr. K. Madlener danke ich fur˜ die Ubernahme der
Zweitbegutachtung meiner Arbeit und die vielen interessanten Diskussionen in den
letzten Jahren. Herr Prof. Dr. A. Poetzsch-Hefiter hat freundlicherweise die Leitung
der Promotionskommision ub˜ ernommen.
Weiterhin m˜ ochte ich mich bei den Kollegen der Arbeitsgruppen von Prof. Avenhaus
und Prof. Madlener fur˜ alle Zusammenarbeit und Diskussion bedanken. In den ersten
Jahren haben mich insbesondere Birgit Reinert, Roland Vogt und Claus-Peter Wirth
in vielen Gespr˜ achen begleitet. In den letzten Jahren haben Tobias Schmidt-Samoa
und Bernd Strieder mich in vielen Dingen tatkr˜ aftig unterstutzt.˜
Waldmeister ist nicht vorstellbar ohne die au…erordentlichen Leistungen von Arnim
Buch, Thomas Hillenbrand und Andreas Jaeger. Vielen Dank fur˜ diesen hervorragen-
den Grundstock meiner praktischen Arbeiten. Die ausgezeichnete Unterstutzung˜ durch
die Studenten Jean-Marie Gaillourdet, Ren¶e Rondot, Christian Schmidt, Hendrik Spies
und Thomas Turk˜ hat mir gerade in praktischen Dingen erheblich weitergeholfen.
Die j˜ahrlichen Beweiserwettbewerbe und das internationale Zusammentrefien mit
an der Implementierung von Beweissystemen interessierten Kollegen waren eine stete
Herausforderung und eine gute Inspirationsquelle. Mein Dank gilt Geofi Sutclifie fur˜
die Organisation und das Design der T-Shirts, sowie Peter Baumgartner, Bill Mc-
Cune, Bernhard Gramlich, Reinhold Letz, Christopher Lynch, Hans de Neville und
Christoph Weidenbach fur˜ viele inspirierende Diskusssionen. Insbesondere danke ich
Thomas Hillenbrand und Stephan Schulz fur˜ die langj˜ahrige gute Zusammenarbeit und
Freundschaft.
Allen, die Teile der Arbeit