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

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).



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

rule1 :-

rule2 :-


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?
• Depending on the problem domain, you might actually get away with verifying solutions on finite sets, in which case the prolog foreach and related functions might suffice. However, I'd first worry about understanding the concepts and gettting enough pen & pencil exercises. Playing with computers is fun, but it can also be a waste of time if you're learning math. Oct 30, 2018 at 20:59