Grundlagen des maschinellen Beweisens: Eine Einführung für Informatiker und Mathematiker

Front Matter....Pages I-IX Grundbegriffe der Prädikatenlogik....Pages 1-31 Resolution....Pages 33-45 Einschränkung des Suchraumes....Pages 47-84 Repräsentation des Suchraums....Pages 85-102 Paramodulation....Pages 103-112 Termersetzung: Grundlagen....Pages 113-128 Termersetzung: Spezielle Techniken....Pages 129-154 Schlußbemerkungen....Pages 155-158 Back Matter....Pages 159-174 Dabei wird ein Bogen von der Resolution über die Paramodulation bis zurTermersetzung gespannt: Der Resolutionskalkül stellt ein handwerkliches Regelsystem für die allgemeine Prädikatenlogik erster Stufe dar, seine Erweiterung um die Paramodulation ermöglicht, die Gleichheitsrelation adäquat behandeln zu können.