Resolution

Zusammenfassung

Wer den Satz von Herbrand und ein widerlegungsadäquates Regelsystem R für variablenfreie Gentzenformeln (z.B. aus dem ersten Kapitel die Schnittregel) kennt, kann mit dem folgenden Verfahren eine beliebige Gentzenformelmenge X in der offenen Prädikatenlogik auf Widersprüchlichkeit hin untersuchen:

• (1) Bilde eine Folge X₀, X₁, X₂,..., so daß

  • X_n eine endliche Teilmenge von grund(X) ist für alle n ∈ ℕ

  • X₀⊊X₁⊊X₂⊊...

  • $\mathop \cup \limits_{n \in {\Bbb N}} {X_n} = grund\left( x \right)$ X_n=grund(X)

• (2) Prüfe sukzessive für n = 0, 1, 2,..., ob X_n ⊢_R□.