Aufgabe:
Text erkannt:
Betrachten Sie die Aussage
- Alle Stürmer können einander gut leiden.
und lösen sie die folgenden Aufgaben.
1. Formalisieren Sie den Satz mit einer Formel in Pränexform unter Verwendung der schon vorhandenen Prädikate.
2. Zeigen Sie mit Hilfe des Grundresolutionsalgorithmus dass die Aussage aus den anderen vier Aussagen folgt. Hinweis:
a) Verwenden Sie die Widerspruchsmethode und zeigen Sie dass \( F_{1} \wedge F_{2} \wedge F_{3} \wedge \) \( F_{4} \wedge \neg F_{5} \) unerfüllbar ist. Dafür:
b) Bringen Sie \( F_{1} \wedge F_{2} \wedge F_{3} \wedge F_{4} \wedge \neg F_{5} \) in Skolemform. Bei der Konjunktion von mehreren Formeln kann man zunächst die Skolemform für jede einzelne Formeln bilden und diese dann zu einer gemeinsamen Skolemform kombinieren. Dabei muss man aber bei verschiedenen Teilformeln unterschiedliche Funktionssymbole verwenden.
c)
d)
e)
f)
Lösung:
1. \( F_{5}=\forall x_{5} \forall y_{5}\left(\left(\right.\right. \) Stuermer \( \left(x_{5}\right) \wedge \) Stuermer \( \left.\left.\left(y_{5}\right)\right) \rightarrow \operatorname{Mag}\left(x_{5}, y_{5}\right)\right) \)
2. a) \( \neg F_{5}=\neg \forall x_{5} \forall y_{5}\left(\left(\right.\right. \)Stuermer\( \left(x_{5}\right) \wedge \)Stuermer \( \left.\left.\left(y_{5}\right)\right) \rightarrow \operatorname{Mag}\left(x_{5}, y_{5}\right)\right) \equiv \exists x_{5} \exists y_{5}\left(\right. \)Stuermer\( \left(x_{5}\right) \wedge \)
Stuermer \( \left.\left(y_{5}\right) \wedge \neg \operatorname{Mag}\left(x_{5}, y_{5}\right)\right) \)
Problem/Ansatz:
Bei a): Darf bei der Skolemform der Allquantor nicht negiert sein oder gibt es einen anderen Grund warum man hier "umwandelt"?
