Logik:Prädikatenlogik/Beweisverfahren/Übungsaufgaben

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

Übungen

Übung 4.3

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))))) $

Lösungen

Lösung 4.3

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:

1. $ \left[ p(a,U,U) \right] $
2. $ \left[ \neg p(X,Y,Z), p(s(X),Y,s(Z)) \right] $
3. $ \left[ \neg p(s(s(a)),s(a),s(s(s(a)))) \right] $
   
   
4. $ [p(s(a),U,s(U))]\ res(1,2) mit \left\{ X \rightarrow a , Y \rightarrow U, Z \rightarrow U \right\} $
5. $ [\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\} $
6. $ []\ 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.