Termersetzungssysteme: Theorie, Implementierung, Anwendung

ISBN-13: 9783528056520 / Niemiecki / Miękka / 1998 / 228 str.

Reinhard B. Ndgen

Opis

Das vorliegende Buch ist aus mehreren Vorlesungen hervorgegangen, die ich an der Fakultat fur Informatik der Universitat Tubingen gehalten habe. Diese Vorlesungen richteten sich an Studenten, die Informatik im Haupt- oder Nebenfach studierten. Neben Informatikern konnte dieses Buch aber auch fur alle, die sich mit formalen Systemen beschaftigen, wertvoll sein, insbesondere Mathematiker, Logiker und Sprachwissenschaftler. Das Buch ist eine Einfuhrung in das Gebiet der Termersetzungssysteme. Dennoch setzt es ei nige fundamentale Grundlagen der Informatik voraus. Diese Grundkenntnisse umfassen die Grundlagen des Programmierens, ein intuitives Verstandnis der Pradikatenlogik und gewisse theoretische Grundlagen (Berechenbarkeit und formale Sprachen), so wie es im allgemeinen bis zum Informatikvordiplom (sowohl im Haupt- als auch im Nebenfach) vermittelt wird. Auch wenn dieses Buch zunachst als Einfuhrung in die Termersetzungssysteme gedacht ist, so soll es die Leser letztlich in die Lage versetzen, selbstandig aktuelle Forschungspublika tionen zu studieren. Systeme zu spezifizieren ist eine wichtige Aufgabe in allen Bereichen der Informatik. Die Spezifikation gehort zur Entwurfsphase jedes Projektes und dient als (Vertrags-)Grundlage fur seine Realisierung (Implementierung), ebenso zur Dokumentation, und sie ist ausserst wichtig bei der Wartung eines fertigen Systems. Formale, d. h. mathematisch exakte Spezifi kationen haben den unbestreitbaren Vorteil, dass sie keinerlei Interpretationsspielraum lassen und somit unzweideutig festlegen, was ein System wirklich leisten soll. Leider sind forma 2 le Spezifikationen fur Ungeubte sowohl schwierig zu erstellen als auch zu lesen. Deshalb fehlt oft die Motivation, eine formale Spezifikation zu erstellen."

Recenzje

"It can be recommended to all those interested in an easy to read introduction to term rewriting systems and in hints for a possible implementation." (Zentralblatt MATH Nr. 903)

Spis treści

1 Einleitung.- 1.1 Rechnen mit Regeln.- 1.2 Termersetzungssysteme.- 1.3 Überblick über das Buch.- 2 Terme und Signaturen.- 2.1 Wohlgeformte Terme.- 2.2 Teilterme.- 2.3 Substitutionen.- 2.4 Datenstrukturen für Terme.- 2.4.1 Zeichenkette und Wörterbuch für Symbole.- 2.4.2 Bäume.- 2.4.3 Gerichtete azyklische Graphen.- 2.5 Aufgaben.- 3 Termvergleiche.- 3.1 Termgleichheit.- 3.2 Termverallgemeinerung und Spezialisierung.- 3.3 Darstellung von Termen in ReDuX.- 3.4 Aufgaben.- 4 Termersetzungssysteme.- 4.1 Regeln und Gleichungen.- 4.2 Algebraische Spezifikationen.- 4.3 Die Implementierung von Reduktionen in ReDuX.- 4.4 Literaturhinweise.- 4.5 Aufgaben.- 5 Ordnungsrelationen und Induktion.- 5.1 Wohlfundierte Ordnungen.- 5.2 Wohlfundierte Induktion.- 5.3 Zusammengesetzte Ordnungen.- 5.4 Quasiordnungen.- 5.5 Aufgaben.- 6 Abstrakte Reduktionsrelationen.- 6.1 Reduktions-und Gleichheitsrelationen.- 6.2 Eigenschaften von Reduktionsrelationen.- 6.3 Kriterien für Konfluenz.- 6.4 Literaturhinweise.- 6.5 Aufgaben.- 7 Termination.- 7.1 Unentscheidbarkeit der Terminationseigenschaft.- 7.2 Termordnungen.- 7.3 Simplifikationsordnungen.- 7.3.1 Der Satz von Kruskal.- 7.3.2 Der Terminationssatz von Dershowitz.- 7.4 Implementierbare Termordnungen.- 7.4.1 Knuth-Bendix-Ordnungen.- 7.4.2 Rekursive Pfadordnungen.- 7.4.3 Polynomordnungen.- 7.5 Literaturhinweise.- 7.6 Aufgaben.- 8 Unifikation.- 8.1 Das Lösen von Termgleichungen.- 8.2 Ein Unifikationskalkül.- 8.3 Komplexität des Unifikationsproblems.- 8.4 Literaturhinweise.- 8.5 Aufgaben.- 9 Kritische Gipfel.- 9.1 Vollständige Termersetzungssysteme.- 9.2 Der Satz von Knuth und Bendix.- 9.3 Aufgaben.- 10 Knuth-Bendix-Vervollständigung.- 10.1 Abstrakte Vervollständigung.- 10.2 Die Vervollständigungsprozedur.- 10.3 Beweistransformation.- 10.4 Konfluenzkriterien.- 10.5 Eine Anwendung: die Lösung von Wortproblemen.- 10.5.1 Endlich erzeugte Strukturen.- 10.5.2 Endlich präsentierte Gruppen.- 10.5.3 Das Wortproblem für endlich präsentierte Gruppen.- 10.6 Literaturhinweise.- 10.7 Aufgaben.- 11 Induktive Vervollständigung.- 11.1 Gleichungs- vs. Induktionsbeweise.- 11.2 Grundtermmodelle.- 11.3 Konsistenzbeweise.- 11.4 Induktionslose Induktion.- 11.5 Grundkonfluenzkriterien.- 11.6 Literaturhinweise.- 11.7 Aufgaben.- 12 Assoziativität und Kommutativität.- 12.1 Termvergleiche modulo einer Theorie.- 12.2 AC-Unifikation.- 12.2.1 Der Nur-Variablen-Fall.- 12.2.2 Der allgemeine Fall.- 12.3 T-kompatible Reduktionen.- 12.4 Termination modulo einer Theorie.- 12.5 Die Peterson-und-Stickel-Vervollständigung.- 12.6 AC-vollständige Termersetzungssysteme.- 12.7 Anwendungen von AC-Termersetzung.- 12.7.1 Automatisches Beweisen mit booleschen Ringen.- 12.7.2 Hardware-Verifikation.- 12.8 Literaturhinweise.- 12.9 Aufgaben.- 13 Schlußbemerkungen.- A Anhang: Termersetzungssoftware.- Symbolverzeichnis.

O autorze

PD Dr. Reinhard Bündgen ist Mitarbeiter bei der IBM Deutschland Entwicklung GmbH und Privatdozent an der Fakultät für Informatik der Universität Tübingen.