How do we translate first order logic's universal quantifier (the $\forall$) and the existential quantifier (the $\exists$) to Prolog?

Question

I'm trying to convert some English statements to first order logic statements and I'm trying to use Prolog to verify the translations. My question is: how do I convert a first order logic statement (having $\forall$ and $\exists$ quantifiers) into Prolog rules?

---

For example, there's this English statement:

Every voter votes for a candidate which some voter doesn't vote for.

and here's my translation of the English statement into first order logic:

$$\forall x, y[Voter(x) \land Candidate(y) \land Votes(x, y) \rightarrow \exists z[ Voter(z) \land \lnot Votes(z, y) ] ]$$

Now I'm not sure if this translation is correct. That's what I want to find out. My question is: how do I convert this first order logic statement to a Prolog rule?

---

So first I'm trying to fill a Prolog database with some facts.

human(p1).
human(p2).
human(p3).
human(p4).
human(p5).
human(p6).
human(p7).
human(p8).
human(p9).
%humans who are neither voters nor candidates
human(p10).
human(p11).


%humans who are only voters
voter(p1).
voter(p2).
voter(p3).


%humans who are candidates and voters
voter(p4).
voter(p5).
voter(p6).
candidate(p4).
candidate(p5).
candidate(p6).


%humans who are only candidates
candidate(p7).
candidate(p8).
candidate(p9).


%some random votes
votes(p1, p6).
votes(p2, p6).
votes(p3, p6).
votes(p4, p7).
votes(p5, p8).
votes(p6, p5).

I'm using human, voter, candidate, and votes. Here are some attempts to model the statement into a Prolog rule:

rule1 :-
  foreach((voter(X), candidate(Y), votes(X, Y)),(voter(Z), \+votes(Z, Y))).

rule2 :-
  foreach((human(X), voter(X), candidate(Y), votes(X, Y)),(human(Z), voter(Z), \+votes(Z, Y))).

Answer 1

Prolog does not support arbitrary first-order logic but only a fragment of it known as Horn clauses. These are statements of the form $$\forall x_1, \ldots, x_n \,.\, P(x_1, \ldots, x_n) \Rightarrow q(x_1, \ldots, x_n)$$ where $P$ is built from atomic predicates and conjunctions, and $q$ is an atomic predicate. Not every statement in logic can be converted to this form.

You are suggesting use of foreach. Note that this is not properly a logic quantifier in Prolog, but rather a special-purpose routine which operates on lists. Pure prolog does not have any of this. If you are willing to use lists and to limit attention to only quantification over finite lists of elements, then you can just implement everything easily enough in Prolog using lists and functions on them. But that misses the point of logic programming, does it not?

Answer 2

If your intention is just to check if your translation from English to first order logic is correct, then I think you could put both your answer and the correct answer that is different from yours in CNF using Herbrand's theorem and compare if they are equal.