How to write it in skolem form?(Prolog)

问题:

Translate the following formula into a horn formula in Skolem form:

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

it's translated from german to english, how to write it in horn form and then in skolem form, i didn't find anything on internet...plz help me

回答1:

I will always use the satisfiability preserving version of skolemization, i.e. the one where those are replaced which would become existential quantifiers when moved to the head of the formula.

To make life a bit simpler, let's push the negations to the atoms. We can also see that w doesn't occur in ¬G(x,x)∨¬H(z) and that x,z don't occur in H(w), allowing us to distribute the quantifiers a bit inside.

Then we obtain the formula ∀w¬H(w) ∨ ∃x∀z (G(x,x)∧ H(z)) .

• If we want to refute the formula:

We skolemize ∃x and delete ∀w, ∀z and obtain:

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

after CNF transformation, we have:

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

both clauses have exactly one positive literal, so they are horn clauses. Translated to Prolog syntax we get:

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

• If we want to prove the formula:

We have to negate before we skolemize, leading to:

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

after skolemizing ∃w and ∃z, deleting ∀x and CNF transformation, we obtain:

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

That could be interpreted as a fact h(c) and a query ?- g(X,X), h(f(X)).

To be honest, both variants don't make much sense - the first does not terminate for any input and in the second version, the query will fail because g/2 is not defined.

回答2:

does this page help?

6.3 Convert first-order logic expressions to normal form

回答3:

A horn clause consists of various goals that all have to be satisfied in order for the whole clause to be true.

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

First you want to translate the whole statement to human language for clarity. ¬ means NOT, ∧ means AND and ∨ means OR. The () are used to group goals.

∀w¬∀x∃z

For all w, all NOT x, at least 1 Z. If a w is true, x must be false and there must be at least 1 z.

H(w)

Is w a H? There must be a fact that says H(w) is true in your knowledge base.

¬G(x,x)

Is there a fact G(x,x)? If yes, return false.

¬H(z)

Is there a fact H(z)? If yes, return false.

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

What this says that z is only true if H(w) is true AND either G(x,x) OR H(z) is false.

In Prolog you'd write this as factCheck(W,X,Z) :- h(W), not(g(X,X);not(checkZ(Z)). where Z is a list with at least 1 entry in it. If ANY element in list Z is true, fail.

%is the list empty?
checkZ([])
%is h true for the first element of the list?
checkZ([Head|Tail]) :- h(Head), !.
%remove the first element of the list
checkZ([Head|Tail]) :- checkZ(Tail).