Hi, in den Folien haben wir auf Folie 6.11 ein Beispiel für eine Ableitung mit dem Modus poens:
http://www.informatik.uni-hamburg.de/WSV/teaching/FGI1/universitaet/FGI1_06_logik.pdf

M1={A,A => B, A => C }
sub2(A) = A, sub2(B) = C
sub2({A,A=>B})={A,A=>C} <= M1 (teilmenge von m1 soll das heissen)
M1 |-MP C

und der MP ist:

(A,A=>B)/B

Ich verstehe nicht wie die Substitutionen gewählt werden. Also warum wird A zu A und B zu C obwohl C nicht mal in dem MP drin ist??

Ich steh irgendwie grad aufn Schlauch ;)

Wenn du eine Inferenzregel (bspw. den Modus Ponens) auf eine Formelmenge M anwenden willst, dann musst du eine Substitution sub finden derart, dass sub angewendet auf die Prämissen der Inferenzregeln eine Menge von Formeln ergibt, die Teilmenge der Menge M ist.

Wenn das geht, dann liegt das Muster F_1, …, F_n (das sollen die Prämissen der Inferenzregel sein) in der Formelmenge M vor und dann darfst du sub(G) (wobei G die Konklusion der Inferenzregel ist) aus M ableiten (in einem Schritt).

Komm doch nächsten Freitag in die Tutorien, wir freuen uns da immer über Zulauf und über Fragen [img]http://www.fb18.de/gfx/25.gif[/img]

Fröhliche Grüsse,
Frank