Hi,
kann mir irgendeiner sagen wie man Wahrheitstafeln für prädikatenlogische Formeln erstellen kann???

z.B.ExAyR(x,y)–>AyExR(x,y) E=Existenzquantor
A=allquantor
Wie zeige ich jetzt ob diese Formel gültig kontingent oder unerfüllbar ist????

oder Ex(P(x)–>Ax(P(x))
Dadurch kann ich auch Augabenblatt 12 nicht ganz lösen…Universum und Expansion kriege ich hin aber ein Modell leider nicht…. für jede art von Hilfe bin ich dankbar…

Wahrheitstafeln sind für prädikatenlogische Formeln relativ schwierig, wenn die Interpretation der Symbole noch nicht festgelegt ist.

Zur Prüfung auf Unerfüllbarkeit ist die Resolution ein geeignetes Mittel. Zum Prüfen auf Gültigkeit wird einfach die negierte Formel resolviert. Wenn keins von beidem zum Erfolg führt (und man beweist, dass es nicht zum Erfolg führen kann) ist die Formel kontingent.

Ehrlich gesagt ist mir nicht ganz klar wie ich die obigen Formeln resolvieren soll bzw. wie ich mit den Quantoren umgehen soll.
meinst du das so: ExAyR(x,y) –> AyExR(x,y)
notExAyR(x,y)oder AyExR(x,y)
AxnotAyR(x,y)oder AyExR(x,y)
AxEynotR(x,y)oder AyExR(x,y)
{notR(x,y)} {R(x,y)}also ist die Formel unerfüllbar???

Für die erste: Ex(P(x)–>Ax(P(x)))
Ex(notP(x)—>Ax(P(x)))
{not P(X)} {P(x)} also wieder unerfüllbar???

Spielen die Quantoren keine Rolle???
bzw. wie kommen die Wahrheitstafeln im Aufgabenblatt 12 zustande(sprich Herbrand-Modell)…Danke für die Hilfe, wäre super wenn Du oder ein anderer diese Fragen auch beantworten könnte….

Die Quantoren spielen bei der Resolution eine Rolle.
Bevor Du die Resolution anwendenden kannst, mußt Du Deine Formel skolemisieren, d.h. alle Existenzquantoren eliminieren.
Dann bildest Du die Klauselmenge und kannst diese resolvieren.

Für die Resolution musst du die Formel erst mal in Skolemform bringen (und gegebenenfalls vorher in Bereinigte Pränexform), also alle Existenzquatoren eliminieren, die Allquantoren stehen vorne, die Matrix liegt in KNF vor. Die Formel in Skolemform ist erfüllbarkeitsäquivalent zur Ursprungsformel, d.h. nur für Tests auf (Un-)Erfüllbarkeit sinnvoll. Dann nimmst du die Matrix (d.h. die Formel ohne die verbliebenen Allquantoren) und bildest daraus die Klauselmenge. Bei der Resolution sollte man geeignete Substitutionen wählen.

Das war sozusagen die Kurzform, wie man vorgehen sollte. Wenn dir die ganzen Begriffe nicht so viel sagen, solltest du noch mal das Skript und die entsprechenden Übungsaufgaben durcharbeiten, insbesondere Aufgabenblatt 14 weil da die ganze Resolution durchgegangen wird (gibts alles hier: http://www.informatik.uni-hamburg.de/WSV/f1/ )

Hier ein Beispiel zu posten geht leider nicht, weil es leider viel zu unübersichtlich werden würde.

Zu den Herbrand-Modellen:
Für die Konstanten setzt du in der Interpretation die Konstante selbst ein. Bei den Funktionen setzt du für die Variable Terme aus dem Herbrand-Universum ein. Wenn der Term dann mit der Ursprungsformel übereinstimmt, kommt als Wahrheitswert 1 raus.
Wie das aber bei Aufgabe 2, F1 mit den y-Varianten im einzelnen funktioniert, kann ich nicht mehr sagen, da Herbrand wirklich nicht meine Stärke ist.

Ehrlich gesagt ist mir nicht ganz klar wie ich die obigen Formeln resolvieren soll bzw. wie ich mit den Quantoren umgehen soll.
meinst du das so: ExAyR(x,y) –> AyExR(x,y)
notExAyR(x,y)oder AyExR(x,y)
AxnotAyR(x,y)oder AyExR(x,y)
AxEynotR(x,y)oder AyExR(x,y)
{notR(x,y)} {R(x,y)}also ist die Formel unerfüllbar???

Da ist dir ein kleiner Fehler unterlaufen. Weil du
AxEynotR(x,y) _oder_ AyExR(x,y) hast, wäre das hier allgemeingültig und nicht unerfüllbar.

Wenn du ExAyR(x,y) –> AyExR(x,y) auf Gültigkeit testen willst, musst du erst mal negieren und in BPF bringen:
NOT(ExAy R(x,y) –> AyEx R(x,y))
NOT(NOT(ExAy R(x,y)) oder AyEx R(x,y))
ExAy R(x,y) und NOT(AyEx R(x,y)))
ExAy R(x,y) und Ey NOT Ex R(x,y)
ExAy R(x,y) und EyAx NOT R(x,y)

Variablen umbenennen:
ExAy R(x,y) und EsAt NOT R(t,s)

Skopus erweitern:
ExAy (R(x,y) und EsAt NOT R(t,s))
ExEsAyAt (R(x,y) und NOT R(t,s))
In diesem Fall kann man Es nach vorne ziehen, weil es nicht vom Allquantor abhängig ist.

Skolemisierung:
EsAyAt (R(a,y) und NOT R(t,s))
AyAt (R(a,y) und NOT R(t,b))

Klauselmenge: {R(a,y)} {R(t,b)}
mit Substitutionen [y/b][t/a] ergibt sich die leere Klausel. Also unerfüllbar und damit hätten wir die Gültigkeit von ExAyR(x,y) –> AyExR(x,y) bewiesen (was zutreffend ist, wie man sich überlegen kann).