# 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?

• Thank you so much for the answer and sorry for the late reply. Can you suggest another logical programming language where one can directly translate first order logic statements to code? – Mina Michael Oct 29 '18 at 20:56
• There isn't one that would do that directly for infinite domains, as that would lead to trying to compute non-computable problems. If you explain what it is that you are trying to really accomplish, there might be tools other than programming languages. – Andrej Bauer Oct 29 '18 at 21:40
• I suppose what I'm asking is: why are you trying to translate English to first-order logic? What will you do with these translations once you've got them? – Andrej Bauer Oct 29 '18 at 21:41
• I'm actually taking an "Introduction to AI" course, and we're learning about first order logic. There are practice assignments with first order logic problems with model answers. Sometimes my solutions are different than those in the model answers. So I want to be able to model the problems and verify my solutions. – Mina Michael Oct 30 '18 at 18:14
• 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. – Andrej Bauer Oct 30 '18 at 20:59

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.