Wie schreibe ich es in Skolemform? (Prolog)

Ich werde immer die Version der Skolemisierung verwenden, bei der die Erfüllbarkeit erhalten bleibt, dh die, bei der diejenigen ersetzt werden, die zu existenziellen Quantifizierern werden, wenn sie an den Kopf der Formel verschoben werden.

Um das Leben ein bisschen einfacher zu machen, lassen Sie uns die Negationen auf die Atome übertragen. Wir können auch sehen, dass w nicht in ¬G (x, x) ∨¬H (z) vorkommt und dass x, z nicht in H (w) vorkommt, was es uns ermöglicht, die Quantifizierer ein wenig im Inneren zu verteilen.

Dann erhalten wir die Formel ∀w¬H (w) ∨x∃z (G (x, x) ∧H (z)).

• Wenn wir die Formel widerlegen wollen:

Wir skolemisieren ∃x und löschen ∀w, ∀z und erhalten:

¬H (w) ∨ (G (c, c) ∧H (z))

Nach der CNF-Transformation haben wir:

(¬H (w) ∨ G (c, c)) ∧ (¬H (w) ∨ H (z))

Beide Klauseln haben genau ein positives Literal, es handelt sich also um Hornklauseln. Übersetzt in die Prolog-Syntax erhalten wir:

g(c,c) :- h(W).
h(Z) :- h(W).

• Wenn wir die Formel beweisen wollen:

Wir müssen negieren, bevor wir skolemisieren, was zu Folgendem führt:

∃w H (w) ∧x∀z (¬G (x, x) ∨H (z))

Nach der Skolemisierung von ∃w und ∃z, dem Löschen der ∀x- und CNF-Transformation erhalten wir:

H (c) ∧ (¬G (x, x) ∨ ¬H (f (x)))

Das könnte als Tatsache h(c)und Abfrage interpretiert werden?- g(X,X), h(f(X)).

Um ehrlich zu sein, machen beide Varianten wenig Sinn - die erste wird für keine Eingabe beendet und in der zweiten Version schlägt die Abfrage fehl, da sie g/2nicht definiert ist.