The generalized resolution principle. (English) Zbl 0195.31102
Das verallgemeinerte resolution principle ist ein einzelnes Inferenzprinzip und stellt eine natürliche Verallgemeinerung der verschiedenen Versionen und Erweiterungen des resolution principle dar. Zusätzlich enthält es die Aspekte, die für eine automatische Berücksichtigung der Gleichheitsrelation erforderlichsind.
Zunächst wird die vollständige Formulierung eines quantorenfreien Prädikatenkalküls 1. Stufe mit Gleichheit gegeben. Dabei werden Sätze unterschieden in einfache (”ground”) und allgemeine: bei einfachen Sätzen haben die Variablen (individual symbols) eine feste Bedeutung, bei allgemeinen Sätzen sind sie als universell quantifiziert zu betrachten. Entsprechend werden zwei verschiedene Folgerungsbegriffe definiert. Es wird gezeigt, daß einfache Sätze entscheidbar sind. Als nächstes wird der Begriff des Beweises untersucht; auch hier wird wieder unterschieden in einfache und allgemeine Beweise, je nachdem, welcher Folgerungsbegriff zugrundegelegt wird. Semantische Bäume werden definiert als Bäume von Formeln, die eine Reihe von Bedingungen erfüllen, um sicherzustellen, daß beim Weiterverfolgen eines Zweiges mehr Information in einer ausführlichen Beschreibung der Interpretation gewonnen wird. Mit diesen Hilfsmitteln kann das verallgemeinerte resolution principle für einfache Sätze bewiesen werden:
Seien \(A_i\) und \(B_i\) Disjunktionen von Literals. Aus \((A_1\vee B_1) \wedge \ldots \wedge (A_k\vee B_k)\) kann eine ”Resolvente” \((A_1 \vee \ldots \vee A_k \vee B)\) gefolgert werden, wobei \(B\) eine Disjunktion ist, die aus \((B_1 \wedge \ldots \wedge B_k)\)) folgt.
Es wird beschrieben, wie hiermit automatisch der Beweis eines einfachen Satzes erzeugt werden kann. Dieses Ergebnis wird erweitert auf Beweise für allgemeine Sätze; hierzu wird ausführlich auf den Begriff der Substitution eingegangen, sowie die unification procedure angegeben, welche die notwendigen Substitutionen erzeugt. Es wird gezeigt, daß es für jedes Theorem einen Beweis gibt, in dem jeder Schritt eine Anwendung des verallgemeinerten resolution principle ist, d.h. die Vollständigkeit dieses Prinzips. Schließlich wird gezeigt, daß die früheren Formen und Erweiterungen des resolution principle Spezialfälle dieses neuen Prinzips sind.
[Dieser Artikel erschien in dem im Zbl 0187.13206 angezeigten Sammelwerk.]
Zunächst wird die vollständige Formulierung eines quantorenfreien Prädikatenkalküls 1. Stufe mit Gleichheit gegeben. Dabei werden Sätze unterschieden in einfache (”ground”) und allgemeine: bei einfachen Sätzen haben die Variablen (individual symbols) eine feste Bedeutung, bei allgemeinen Sätzen sind sie als universell quantifiziert zu betrachten. Entsprechend werden zwei verschiedene Folgerungsbegriffe definiert. Es wird gezeigt, daß einfache Sätze entscheidbar sind. Als nächstes wird der Begriff des Beweises untersucht; auch hier wird wieder unterschieden in einfache und allgemeine Beweise, je nachdem, welcher Folgerungsbegriff zugrundegelegt wird. Semantische Bäume werden definiert als Bäume von Formeln, die eine Reihe von Bedingungen erfüllen, um sicherzustellen, daß beim Weiterverfolgen eines Zweiges mehr Information in einer ausführlichen Beschreibung der Interpretation gewonnen wird. Mit diesen Hilfsmitteln kann das verallgemeinerte resolution principle für einfache Sätze bewiesen werden:
Seien \(A_i\) und \(B_i\) Disjunktionen von Literals. Aus \((A_1\vee B_1) \wedge \ldots \wedge (A_k\vee B_k)\) kann eine ”Resolvente” \((A_1 \vee \ldots \vee A_k \vee B)\) gefolgert werden, wobei \(B\) eine Disjunktion ist, die aus \((B_1 \wedge \ldots \wedge B_k)\)) folgt.
Es wird beschrieben, wie hiermit automatisch der Beweis eines einfachen Satzes erzeugt werden kann. Dieses Ergebnis wird erweitert auf Beweise für allgemeine Sätze; hierzu wird ausführlich auf den Begriff der Substitution eingegangen, sowie die unification procedure angegeben, welche die notwendigen Substitutionen erzeugt. Es wird gezeigt, daß es für jedes Theorem einen Beweis gibt, in dem jeder Schritt eine Anwendung des verallgemeinerten resolution principle ist, d.h. die Vollständigkeit dieses Prinzips. Schließlich wird gezeigt, daß die früheren Formen und Erweiterungen des resolution principle Spezialfälle dieses neuen Prinzips sind.
[Dieser Artikel erschien in dem im Zbl 0187.13206 angezeigten Sammelwerk.]
Reviewer: G. Veenker
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 68Q55 | Semantics in the theory of computing |
