Bearbeiten von „Logik:Prädikatenlogik/Beweisverfahren/Übungsaufgaben“

= Übungsaufgaben zu [[Logik:Beweisverfahren]] in der [[Logik:Prädikatenlogik]] =

== Übungen ==
=== Übung 4.1 ===

=== Übung 4.2 ===

=== Übung 4.3 ===
Beweisen Sie mit Resolution die Allgemeingültigkeit der Formel<br><br>

<math>

(((\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)))))

</math>
== Lösungen ==
=== Lösung 4.2 ===
=== Lösung 4.1 ===
=== 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:Implikation]]en umgewandelt. Am Ende schreiben wir die Formel in [[Logik:Klauselform]].


<math>

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

</math>


<math>

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

</math>


<math>

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

</math>


<math>

(((\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)))))

</math>


<math>

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

</math>


<math>

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

</math>


<math>

\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

</math>


Jetzt in die Schreibweise und [[Logik:Resolutionsverfahren|Resolution]] durchführen:


#<math>

\left[ p(a,U,U) \right]

</math>
#<math>

\left[ \neg p(X,Y,Z), p(s(X),Y,s(Z)) \right]

</math>
#<math>

\left[ \neg p(s(s(a)),s(a),s(s(s(a)))) \right]

</math><br><br>
#<math>

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

</math>
#<math>

[\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\} 

</math>
#<math>

[]\ res(4,5) mit \left\{ U \rightarrow s(a) \right\} 

</math>

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

[[Kategorie:Logikaufgaben]]