Resolventenbildung; zwei Klauseln mit zwei Fragen und Antworten gesucht

Question

Aufgabe:

Resolventen bilden:

Ich suche die leere Menge.

{¬m(x), e(x)}           {m(z), e(z)}

                            {m(x), e(x)}

Nun ist meine Frage: Was erhalte ich hierbei?

Frage 1:

{e(x), e(x)} ?

Und was kommt bei:

{¬m(x), e(x)} {m(x), ¬e(z)} für ein Resolvent raus? Kann man beide kürzen?

Answer 1

Frage 1: Resolvent von \(e(x), e(x)\)

Ergebnis: \(e(x)\)

Die Klausel bleibt logisch äquivalent, da \( e(x) \lor e(x) \equiv e(x) \).

Frage 2: Resolvent von \(¬m(x), e(x)\) und \(m(x), ¬e(z)\)

Schritt 1: Unifikation der Literale \( \neg m(x) \) und \( m(x) \).

Schritt 2: Resolutionsschritt:
Entferne \( \neg m(x) \) und \( m(x) \) aus den Klauseln.
Kombiniere die restlichen Literale: \( e(x) \) und \( \neg e(z) \).

Schritt 3: Unifikation von \( e(x) \) und \( \neg e(z) \):
Substituiere \( z \) durch \( x \).

Ergebnis: \( e(x) \) und \( \neg e(x) \) widersprechen sich direkt.

Finaler Resolvent: Die leere Menge \(\{\}\) (Widerspruch).

Kürzen der Literale?

Ja, durch Unifikation und Resolution entsteht die leere Klausel, die den Widerspruch darstellt.