Inhaltsverzeichnis

Übungsaufgaben zu Logik:Beweisverfahren in der Logik:Prädikatenlogik

Beweisen Sie mit Resolution die Allgemeingültigkeit der Formel

$ (((\forall X)p(a,X,X)\and(\forall X)(\forall Y)(\forall Z)(p(X,Y,Z)\rightarrow p(s(X),Y,s(Z))))\rightarrow p(s(s(a)),s(a),s(s(s(a))))) $

Um Logik:Allgemeingültigkeit zu beweisen gibt es mehrere Logik:Beweisverfahren. Das hier geforderte Logik:Resolutionsverfahren beruht auf einen negativen, analysierenden Logik:Kalkül. Wenn wir doppelt gebundene Variablen umbenannt haben, negieren wir die Formel und ziehen wir die Logik:Quantoren heraus. Nun werden die Logik:Implikationen umgewandelt. Am Ende schreiben wir die Formel in Logik:Klauselform.

$ \neg(((\forall U)p(a,U,U)\and(\forall X)(\forall Y)(\forall Z)(p(X,Y,Z)\rightarrow p(s(X),Y,s(Z))))\rightarrow p(s(s(a)),s(a),s(s(s(a))))) $

$ \neg(((\forall U)(\forall X)(\forall Y)(\forall Z)p(a,U,U)\and(p(X,Y,Z)\rightarrow p(s(X),Y,s(Z))))\rightarrow p(s(s(a)),s(a),s(s(s(a))))) $

$ \neg(\neg((\forall U)(\forall X)(\forall Y)(\forall Z)p(a,U,U)\and(p(X,Y,Z)\rightarrow p(s(X),Y,s(Z))))\or p(s(s(a)),s(a),s(s(s(a))))) $

$ (((\forall U)(\forall X)(\forall Y)(\forall Z)p(a,U,U)\and(p(X,Y,Z)\rightarrow p(s(X),Y,s(Z))))\and \neg p(s(s(a)),s(a),s(s(s(a))))) $

$ ((p(a,U,U)\and(p(X,Y,Z)\rightarrow p(s(X),Y,s(Z))))\and \neg p(s(s(a)),s(a),s(s(s(a))))) $

$ ((p(a,U,U)\and(\neg p(X,Y,Z)\or p(s(X),Y,s(Z))))\and \neg p(s(s(a)),s(a),s(s(s(a))))) $

$ \left\langle \left[ p(a,U,U) \right], \left[ \neg p(X,Y,Z), p(s(X),Y,s(Z)) \right], \left[ \neg p(s(s(a)),s(a),s(s(s(a)))) \right] \right\rangle $

Jetzt in die Schreibweise und Resolution durchführen:

$ \left[ p(a,U,U) \right] $
$ \left[ \neg p(X,Y,Z), p(s(X),Y,s(Z)) \right] $
$ \left[ \neg p(s(s(a)),s(a),s(s(s(a)))) \right] $
$ [p(s(a),U,s(U))]\ res(1,2) mit \left\{ X \rightarrow a , Y \rightarrow U, Z \rightarrow U \right\} $
$ [\neg p(s(a),s(a),s(s(a))]\ res(2,3) mit \left\{ X \rightarrow s(a), Y \rightarrow s(a), Z \rightarrow s(s(a)) \right\} $
$ []\ res(4,5) mit \left\{ U \rightarrow s(a) \right\} $

Wir erhalten den Widerspruch in Zeile 5 mit $ [] $. Da wir unsere Aussage vorher negiert haben, haben wir die Logik:Allgemeingültigkeit bewiesen.