FB18 - Das Forum für Informatik

fb18.de / Diplom Informatik / Unterbereich Grundstudium / Formale Informatik

Modus Ponens

Modus Ponens 2005-10-08 20:47
Anonymer User
Kann mir einer Anhand der Aufgabe 1 auf Zettel 6 (F1) sagne wie er auf (F->F) kommt?
man soll das mithilfe des MP aus der leeren Menge folgern. Kann mir einer mal generel sagen wie man den MP anwendet? Vielen Dank im vorraus

Re: Modus Ponens 2005-10-09 04:48
georg
Ah, du meinst wohl die Aufgaben vom WiSe 03/04.
Dazu habe ich nur noch meine Lösung von damals
und weiß nicht sicher, ob sie richtig ist. Am
besten postest du mal das Axiomensystem, dann
kann ich nachsehen, ob meine Lösung richtig war
und sie ggf. hier reinschreiben.

Zum Modus Ponens allgemein: Bei dieser Aufgabe
geht es um das Ableiten in einem Kalkül (und
zwar mit einem, das MP als einzige Inferenzregel
enthält). Wie man das macht, ist in Definition
6.10 beschrieben: man erweitert einen Satz von
Formeln schrittweise um eine weitere Formel, indem
man jedes Mal eine von drei Aktionen durchführt:
1) Verwenden einer Formel aus M
2) Substituieren in einem Axiom
3) Anwenden einer Inferenzregel auf die bisher
abgeleiteten Formeln.

An welcher Stelle hast du denn Schwierigkeiten?

Re: Modus Ponens 2005-10-09 15:51
Anonymer User
Und zwar sind die folgenden 3 Axiome gegeben die man vorher auch beweisen hat mithilfe von Wahrheitstabellen:

A1: (A->(B->A))
A2: (A->(B->C))->((A->B)->(A->C)))
A3: ((-A-> -B)->(B->A))

Aufgabe: Zeigen Sie, daß man mit Substitution und Anwendung der Regel MP die folgenden Formeln aus der leeren menge ableiten kann.

a. (A->A)
b. (-A->(A->B))
c. (–A->A)
d. (A-> –A)

wobei ich schon bei a. nicht ganz verstehe wie er auf A->A kommt. Vielen Dank im vorraus

Re: Modus Ponens 2005-10-09 23:15
georg
OK, dann wollen wir mal.

Zunächst setzen wir sub1(A)=sub1(C)=A, sub1(B)=B->A. Dann
erhalten wir
[img]http://mokrates.de/cgi-bin/texstring?F_1%3D((A%5Crightarrow%20((B%5Crightarrow%20A)%5Crightarrow%20A))%5Crightarrow%20((A%5Crightarrow(B%5Crightarrow%20A))%5Crightarrow(A%5Crightarrow%20A)))%3D%5Cmathtt%7Bsub%7D_1(A_2)[/img]
(obige Aktion 2).

[img]http://mokrates.de/cgi-bin/texstring?F_2%3D(A%5Crightarrow((B%5Crightarrow%20A)%5Crightarrow%20A))%3D%5Cmathtt%7Bsub%7D_1(A_1)[/img]
(Aktion 2)

[img]http://mokrates.de/cgi-bin/texstring?F_3%3D((A%5Crightarrow%20(B%5Crightarrow%20A))%5Crightarrow(A%5Crightarrow%20A))[/img]
(Aktion 3: MP angewendet auf F2, F1)

[img]http://mokrates.de/cgi-bin/texstring?F_4%3D(A%5Crightarrow%20(B%5Crightarrow%20A))%3D%5Cmathtt%7Bid%7D(A_1)[/img]
(wieder Aktion 2, diesmal mit der Substitution, die
nichts verändert).

Und jetzt ist klar, was kommt:
[img]http://mokrates.de/cgi-bin/texstring?F_5%3D(A%5Crightarrow%20A)[/img]
(Aktion 3: MP angewendet auf F4, F3)

Die Substitutionen beim MP sind bestimmt klar,
sonst frag einfach nach.

Re: Modus Ponens 2005-10-10 19:19
Anonymer User
Ah! Jetzt hab ichs.. einfaches Patternmatching :D Vielen Dank!