Grundlagen Des Maschinellen Beweisens: Eine Einführung Für Informatiker Und Mathematiker

ISBN-13: 9783528147181 / Niemiecki / Miękka / 1991 / 174 str.

Ralf-Detlef Kutsche; Dieter Hofbauer

Opis

Dieses Buch ist ein Lehrbuch, das prazise die logischen und mathematischen Grundlagen des automatischen Theorembeweisens entwickelt. Es richtet sich an Studenten und Wissenschaftler der Informatik, die damit auch Grundlagen von Symbolmanipulation, formalen Spezifikationsmethoden sowie funktionaler und logischer Programmierung erwerben konnen.Ausgehend von der Pradikatenlogik werden theoretische Konzepte und Strategien fur automatische Theorembeweiser vorgestellt. Dabei wird ein Bogen von der Resolution uber die Paramodulation bis zurTermersetzung gespannt: Der Resolutionskalkul stellt ein handwerkliches Regelsystem fur die allgemeine Pradikatenlogik erster Stufe dar, seine Erweiterung um die Paramodulation ermoglicht, die Gleichheitsrelation adaquat behandeln zu konnen. (, Ersetzen von Gleichem durch Gleiches"); schliesslich wird mit der ausfuhrlichen Behandlung von Termersetzungssystemen eine operationale Sichtweise von reinen Gleichungsmengen betont."

Spis treści

l Grundbegriffe der Prädikatenlogik.- 1.1 Syntax der Prädikatenlogik.- 1.2 Semantik der Prädikatenlogik.- 1.3 Normierung der Syntax: Gentzenformeln und die Schnittregel.- 1.4 Normierung der Semantik: Herbrand-Strukturen.- 1.5 Korrektheit und Vollständigkeit.- 1.6 Theorembeweisen durch Widerlegungen.- 2 Resolution.- 2.1 Unifikation.- 2.2 Resolution und Faktorisierung.- 3 Einschränkung des Suchraums.- 3.1 Der Suchraum.- 3.2 Allgemeine Konzepte.- 3.3 Strukturelle Konzepte.- 3.4 Ordnungskonzepte.- 3.5 Semantische Konzepte.- 3.6 Kombination von Konzepten.- 4 Repräsentation des Suchraums.- 4.1 Connection-Graph-Resolution.- 4.2 Matrix-Verfahren.- 4.3 Tableau-Verfahren.- 5 Paramodulation.- 5.1 Gleichheit.- 5.2 Paramodulation.- 6 Termersetzung: Grundlagen.- 6.1 Termersetzungssysteme.- 6.2 Ersetzungssysteme: Termination und Konfluenz.- 6.3 Lokale Konfluenz und kritische Paare.- 7 Termersetzung: Spezielle Techniken.- 7.1 Terminationskriterien.- 7.2 Knuth-Bendix-Vervollständigung.- 7.3 Induktive Beweise.- 7.4 Lösen von Gleichungen: Narrowing.- 7.5 Beweisen in speziellen Gleichheitstheorien.- Schlußbemerkungen.- Literatur.- Symbolverzeichnis.- Sachwortverzeichnis.