Reduktionssysteme Rechnen und Schließen in gleichungsdefinierten Strukturen

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 von grundlegenden Eigenschaften.
Das Buch eignet sich für eine Vorlesung im Informatik-Hauptstudium. Durch Beispiele und Übungsaufgaben wird die anschauliche und übersichtliche Darstellung abgerundet.
Für Studenten und Wissenschaftler auf dem Gebiet der Mathematischen Logik und formalen Sprachen, der Logik und Semantik von Programmiersprachen und der künstlichen Intelligenz.