Logik:Klausuren/07.02.2004/1.4 Aufgabe
Inhaltsverzeichnis
1. Aufgabenstellung
Wie bei der Behandlung des Ersetzungstheorems bezeichne $ F[G]\; $ eine aussagenlogische Formel $ F\; $ mit der Teilformel $ G\; $ und $ F[G/H]\; $ die Formel $ F\; $, in der alle Teilformeln $ G\; $ durch die Formel $ H\; $ ersetzt werden.
a) Gilt für beliebige aussagenlogische Formeln $ F\; $, $ G\; $ und $ H\; $ die Beziehung $ \{G\rightarrow H\} \models (F[G]\rightarrow F[G/H]) $? Beweisen Sie Ihre Antwort.
b) Schreiben Sie ein Prologprogramm $ ers(F,G,H,Fneu)\; $, das in einer gegebenen Formel $ F\; $ alle Teilformeln $ G\; $ durch eine vorgegebene Formel $ H\; $ ersetzt und die transformierte Formel $ Fneu\; $ liefert.
Z.B. soll der Aufruf
$ \mathsf{?- ers(((p\ and\ q)\ or\ (p\ and\ q)),\ (p\ and\ q),\ (r\ or\ p),\ Fneu).} $
die Antwort $ \mathsf{Fneu\ =\ ((r\ or\ p)\ or\ (r\ or\ p))} $ geben.
Beschränken Sie sich auf Formeln mit den Junktoren $ \and ,\or $ und $ \neg\; $, deren Prologdefinition durch $ \mathsf{:-op(10,fx,neg). :-op(20,xfx,[and,or]).} $ vorgegeben ist.
2. Lösung
a)
Nein, Gegenbeispiel:
$ F = \neg (p \and q),\ G = (p \and q),\ H = p $
$ F[G/H] = \neg p $
Wähle $ I\; $ mit $ p^I = w, q^I = f\; $
$ (G\rightarrow H)^I $
$ \equiv ((p \and q)\rightarrow p)^I $
$ \equiv ((w \and * f)\rightarrow * w) $
$ \equiv w $ (1)
$ (F[G]\rightarrow F[G/H])^I $
$ \equiv (\neg *(p \and q)\rightarrow \neg p)^I $
$ \equiv (\neg *(w \and * f)\rightarrow * \neg * w) $
$ \equiv (\neg * f\rightarrow * \neg * w) $
$ \equiv (w \rightarrow * f) $
$ \equiv f $ (2)
Aus (1) und (2) folgt ein Widerspruch.
b)
$ \mathsf{ers(F,F,H,H)\ :-\ !.} $
$ \mathsf{ers(F,G,H,F)\ :-\ atomic(F).} $
$ \mathsf{ers(neg\ F,G,H,neg\ Fneu)\ :-\ ers(F,G,H,Fneu).} $
$ \mathsf{ers((F1\ and\ F2),G,H,(F1neu\ and\ F2neu))\ :-\ ers(F1,G,H,F1neu), ers(F2,G,H,F2neu).} $
$ \mathsf{ers((F1\ or\ F2),G,H,(F1neu\ or\ F2neu))\ :-\ ers(F1,G,H,F1neu), ers(F2,G,H,F2neu).} $
3. Lösungsweg
4. Alternativen/Diskussion/Hinweise etc.
a)
Aussage gilt nicht.
Gegenbeispiel:
$ G = (p \and \neg p) $ unerfüllbar
$ H = (p \or \neg p) $ Tautologie
$ F[G] = \neg (p \and \neg p) $ Tautologie
$ F[G/H] = \neg (p \or \neg p) $ unerfüllbar
Aussage gilt gdw. $ ((G \rightarrow H) \rightarrow (F[G] \rightarrow F[G/H])) $ Tautologie,
aber: $ ((f \rightarrow * w) \rightarrow * (w \rightarrow * f)) = (w \rightarrow * f) = f $
b)
$ \mathsf{ers(F, F, G, G)\ :-\ !.} $
$ \mathsf{ers(F,\_,\_,F)\ :-\ atomic(F).} $
$ \mathsf{ers(neg\ F, A, B, neg\ Fneu)\ :-\ ers(F, A, B, Fneu),\ !.} $
$ \mathsf{ers(F, A, B, Fneu)\ :-\ F =.. [J, G, H],\ member(J, [and, or]),\ ers(G, A, B, Gneu),\ ers(H, A, B, Hneu),\ Fneu =.. [J, Gneu, Hneu].} $
zur Klausur 07.02.2004
Aufgaben-Kategorie AL - Äquivalenz und NormalformenAufgaben-Kategorie Prolog