Blick ins Buch

Reduktionssysteme

Rechnen und Schließen in gleichungsdefinierten Strukturen

Jürgen Avenhaus (Autor)

Buch | Softcover

X, 251 Seiten

1995
Springer Berlin (Verlag)
9783540585596 (ISBN)

Lese- und Medienproben

Inhaltsverzeichnis (PDF)

Artikel merken

Reduktions- und Vervollständigungstechniken dienen zum Rechnen und Schließen in gleichungsdefinierten algebraischen Strukturen wie Abstrakten Datentypen. In dieser ersten systematischen Einführung in das Gebiet der Reduktionssysteme werden die Grundlagen entwickelt und auf unterschiedliche Ersetzungssysteme angewandt. Themenschwerpunkte sind: 1. denotationale, operationale und rewrite-basierte Semantik, 2. effiziente und nachweisbar korrekte Vervollständigungsalgorithmen, 3. Inferenzsysteme, die auf Beweistransformation und Beweisordnung basieren, und 4. prinzipielle Entscheidbarkeit grundlegender Eigenschaften.
Das Buch eignet sich für eine Vorlesung im Informatik-Hauptstudium. Durch Beispiele und Übungsaufgaben wird die anschauliche, übersichtliche Darstellung abgerundet.

0 Einleitung.- 0.1 Motivation.- 0.2 Termersetzungssysteme und abstrakte Datentypen.- 1 Abstrakte Reduktionssysteme.- 1.1 Definitionen und erste Ergebnisse.- 1.2 Konfluenz und die Church-Rosser-Eigenschaft.- 1.3 Konstruktion von Noetherschen Partialordnungen.- 1.4 Konstruktion von konvergenten Reduktionssystemen.- 2 Wortersetzungssysteme.- 2.1 Motivation.- 2.2 Termination und Konfluenz.- 2.3 Die Vervollständigung nach Knuth-Bendix.- 2.4 Entscheidbarkeitsfragen.- 3 Termersetzungssysteme.- 3.1 Motivation.- 3.2 Spezifikation von Datentypen.- 3.3 Termersetzungssysteme.- 3.4 Matching und Unifikation.- 3.5 Konfluenz und Termination.- 3.6 Die Vervollständigung nach Knuth-Bendix.- 3.7 Reduktionsordnungen.- 3.8 Modularität.- 4 Termersetzung modulo einer Kongruenz.- 4.1 Die Church-Rosser-Eigenschaft modulo A.- 4.2 A-Vervollständigung für links-lineare Regeln.- 4.3 A-Vervollständigung für beliebige Regeln.- 4.4 A-verträgliche Reduktionsordnungen.- 5 Ausblick.- Wegweiser zur Originalliteratur.

Erscheint lt. Verlag	6.3.1995
Reihe/Serie	Springer-Lehrbuch
Zusatzinfo	X, 251 S. 5 Abb.
Verlagsort	Berlin
Sprache	deutsch
Maße	155 x 235 mm
Gewicht	406 g
Themenwelt	Mathematik / Informatik ► Informatik ► Theorie / Studium
Schlagworte	Abstrakte Datentypen • Algebra • Algebraische Semantik • Assoziativgesetz • Automatisches Beweisen • Automatisches Beweisverfahren • Beweis • Datentyp • Gleichung • HC/Informatik, EDV/Informatik • Knuth-Bendix-Vervollständigung • Rechnen • Reduktionssystem • Reduktionssysteme • Relationen • Termersetzungssysteme
ISBN-13	9783540585596 / 9783540585596
Zustand	Neuware