Logisches Schließen und Theorembeweisen

Logisches Schließen und Theorembeweisen befassen sich mit der Verwendung formaler Logik zur Wissensrepräsentation und der Automatisierung von Deduktion, wobei Schlussfolgerungen abgeleitet werden, die notwendigerweise aus einer Menge von Prämissen folgen.

Definition

Theorembeweisen ist die automatisierte Ableitung, ob eine logische Formel aus einer Menge von Axiomen folgt, typischerweise durch Manipulation der Formeln mit korrekten Inferenzregeln, bis das Ziel abgeleitet oder ein Widerspruch erreicht wird.

Scope

Dieses Thema behandelt das Schließen in der Aussagen- und Prädikatenlogik sowie die Algorithmen, die es automatisieren: Wahrheitswerttabellen und DPLL-basierte Erfüllbarkeitsprüfung für die Aussagenlogik, Unifikation und das Resolutionsprinzip für die Prädikatenlogik, Vorwärts- und Rückwärtsverkettung sowie die Grundlagen der logischen Programmierung. Es befasst sich mit der Korrektheit, Vollständigkeit und Entscheidbarkeit von Inferenzverfahren. Das Schließen, das Unsicherheiten oder Standardwerte toleriert, wird in den verwandten Themen zum Schließen unter Unsicherheit und nicht-monotonen Schließen behandelt.

Core questions

• Was bedeutet es, wenn eine Schlussfolgerung aus einer Menge von Prämissen folgt, und wie wird diese Folgerung mechanisch überprüft?
• Wie liefert das Resolutionsprinzip mit Unifikation eine einzige vollständige Inferenzregel für die Prädikatenlogik?
• Wie unterscheiden sich Vorwärts- und Rückwärtsverkettung als Inferenzstrategien?
• Was sind die Grenzen des automatisierten Schließens, angesichts der Tatsache, dass die Gültigkeit erster Ordnung nur semi-entscheidbar ist?

Key concepts

• Aussagen- und Prädikatenlogik
• Folgerung und Gültigkeit
• Unifikation
• Resolution und Widerlegung
• DPLL und SAT-Lösen
• Vorwärts- und Rückwärtsverkettung
• Horn-Klauseln und logische Programmierung
• Korrektheit und Vollständigkeit

Key theories

Resolutionsprinzip

Robinsons Resolution ist eine einzelne Inferenzregel für Klauseln, die, kombiniert mit Unifikation, widerlegungsvollständig für die Prädikatenlogik ist: Jede unerfüllbare Menge von Klauseln kann durch Ableitung der leeren Klausel als unerfüllbar gezeigt werden.

DPLL und aussagenlogische Erfüllbarkeit

Das Davis-Putnam-Verfahren und seine DPLL-Verfeinerung entscheiden die aussagenlogische Erfüllbarkeit durch systematische Fallunterscheidung mit Einheitsausbreitung und reiner Literalen-Eliminierung, was die Grundlage moderner SAT-Löser bildet.

Logische Programmierung und Rückwärtsverkettung

Die Beschränkung der Prädikatenlogik auf Horn-Klauseln und die Rückwärtsauflösung von Zielen führt zur logischen Programmierung, bei der die Berechnung eine Beweissuche ist, was sowohl eine Schlussfolgerungsmethode als auch ein Programmierparadigma darstellt.

Clinical relevance

Automatisiertes Theorembeweisen und SAT/SMT-Lösen werden in der Hardware- und Software-Verifikation, Programmanalyse, Planung und Mathematik eingesetzt, während logische Programmiersprachen wie Prolog die Rückwärtsverkettungsinferenz auf Datenbanken, Parsing und regelbasierte Systeme anwenden.

History

Frühe Beweisverfahren von Gilmore, Davis und Putnam (1960) automatisierten das aussagenlogische und quantorenlogische Schließen, und Robinsons Resolutionsprinzip (1965) vereinte die Inferenz erster Ordnung in einer Regel. In den 1970er Jahren wurde die Resolution zur logischen Programmierung und Prolog verfeinert; SAT- und SMT-Lösen entwickelten sich später zu einer wichtigen praktischen Technologie.

Key figures

• John Alan Robinson
• Martin Davis
• Hilary Putnam
• Robert Kowalski
• Alan Robinson

Seminal works

• robinson1965
• davis1960
• kowalski1979

Frequently asked questions

Was ist das Resolutionsprinzip?

Resolution ist eine einzelne Inferenzregel, die zwei Klauseln mit komplementären Literalen nimmt und eine neue Klausel erzeugt, die den Rest kombiniert. Wiederholt angewendet mit Unifikation, kann sie zeigen, dass eine Menge von Klauseln erster Ordnung unerfüllbar ist, was die Grundlage für das Beweisen von Theoremen durch Widerlegung ist.

Ist die automatisierte Theorembeweisführung garantiert terminierend?

Für die Aussagenlogik ist die Gültigkeit entscheidbar, daher terminieren die Verfahren. Für die vollständige Prädikatenlogik ist die Gültigkeit nur semi-entscheidbar: Ein vollständiger Beweiser wird jede gültige Formel schließlich bestätigen, kann aber bei einer ungültigen Formel ewig laufen, sodass die Terminierung im Allgemeinen nicht garantiert ist.