Grundlagen des maschinellen Beweisens

Dieses Buch ist ein Lehrbuch, das przise 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 knnen.Ausgehend von der Prdikatenlogik werden theoretische Konzepte und Strategien fr automatische Theorembeweiser vorgestellt. Dabei wird ein Bogen von der Resolution ber die Paramodulation bis zurTermersetzung gespannt: Der Resolutionskalkl stellt ein handwerkliches Regelsystem fr die allgemeine Prdikatenlogik erster Stufe dar, seine Erweiterung um die Paramodulation ermglicht, die Gleichheitsrelation adquat behandeln zu knnen. (,, Ersetzen von Gleichem durch Gleiches"); schlielich wird mit der ausfhrlichen Behandlung von Termersetzungssystemen eine operationale Sichtweise von reinen Gleichungsmengen betont.