Short notes on Prolog

The following notes aim just at giving a rough (and somewhat not formal) idea of how and why the programming language Prolog works.

Prolog is a programming language based on a fragment of first-order predicate logic.

Formulas of first-order logic are formed using basic predicates (and terms), logical connectives and quantifiers.
A basic predicate is used to represent a basic statement about individual elements of the domain we are taking into account. The elements of the domain are denoted by terms.
For instance: even(2), divisible(15,3), greaterThan(5*7,1+1) etc. .
In Prolog, basic predicates are denoted by identifiers beginning with lower case letters. Terms denoting elements of the domain are formed using variables, constants and function symbols.
In Prolog, variables are represended by identifiers beginning with a upper-case letter, whereas constants and function symbols are represented by identifiers starting with lower-case letters. The following is a possible term in Prolog notation: f(Y,g(X,c)). An example of basic statement formed using the basic binary predicate pred(_,_) and the terms f(Y,g,(X,c)) and Z is pred(f(Y,g,(X,c)),Z) (basic statements are also called atomic formulas).
In first-order logic more complex formulas can be defined by means of Logical Connectives: And ( ∧ ), Or ( ∨ ), Implies (→) etc.

In the following a generic formula will be denoted by A,B, etc. We write A(X) to represent that the formula A contains a predicate which uses a variable X.

In first-order logic, formulas can be universally or existentially quantified:

• the formula ∀X.A(X) means that the A(X) holds for any possible element X of the domain:
• the formula ∃X.A(X) means that there exists an element t of the domain such that A(t) holds.

The quantifiers are binders for the quantified variables, like the 'λ' for λ-terms. So quantified formulas have to be considered modulo α-conversion (∀X.A(X) is the very same formula as ∀Y.A(Y)).

Given a formula A it is not possible, in general, to decide whether there is a proof for A (i.e. A is derivable) in first-order logic. In other words, there is no algorithm whatsoever which, given a formula A, terminates telling us if A is derivable or not (or, equivalently, if A is valid or not).

The following are some of the rules of first-order logic that can be used to prove formulas:

Modus Ponens:

∀-Elimination: ∃-Introduction: ∧-Introduction :

Even if first-order logic is undecidable, there are however fragments of it that are decidable. Other ones, even if not decidable, allow for semi-decision algorithms that are extremely efficient. One of these is the fragment where we consider only formulas with the following shape

or with the shape
where

• A₁, A₂,..., A_n, B, C are atomic formulas;
• the variables occurring in B have to be considered universally quantified in
  (A₁ ∧ A₂ ∧ .... ∧ A_n) → B and in B;
• the variables occurring in A₁, A₂,..., A_n but not in B have to be considered existentially quantified in (A₁ ∧ A₂ ∧ .... ∧ A_n).
• the variables occurring in C have to be considered universally quantified;

Formulas of these forms are called Horn Clauses.
Notice that instead of considering the above quantifications, we can consider all the variables in C and (A₁ ∧ A₂ ∧ .... ∧ A_n) → B to be universally quantified
(since in first order logic, when Y is not a free variable in Q, ∀X.( (∃Y.P)→Q ) is logically equivalent to ∀X,Y.( P→Q), see (5) of Proposizione 2 in [AU] ).

In Prolog, a formula (A₁ ∧ A₂ ∧ .... ∧ A_n) → B is represented as

B :- A1, A2,..., An

An example of Horn Clause in Prolog is

c(X,f(Y)) :- a(X,Y), b(g(Z),s), d(Z,Z).

(Horn Clauses in Prolog always terminate with a dot '.')

In the above formula all the variables are considered to be quantified as explained before. So the corresponding formula in logic notation would be

If one takes a set of Horn clauses H₁,..,H_n, and a formula of the form

where B is an atomic formula there exists an algorithm which, in case this formula is derivable from the hypotheses H₁,..,H_n, finds a proof for it in an efficient way (such algorithm is called Resolution Algorithm).

Even more, it can find out all the possible proofs if there is more than one.

In Prolog the formula ∃X₁,..,X_k.B is represented simply by B and it is usually written after the prompt of the interpreter '?-', as follows

?- B.

B is called Goal.

Let us consider a few clauses, like in [ACa,], in particular the facts

animal(lion).
animal(dog).
animal(sparrow).
animal(seagull).
has_feathers(sparrow).
has_feathers(seagull).

and the clause

   bird(X) :-
   animal(X),
   has_feathers(X).

If we make the following query to the Prolog interpreter

?- bird(Z)

is like asking the Prolog interpreter for a proof of where Γ is the set of the above facts.

The interpreter finds a proof of it, something like THIS.
and returns us what the possible bird is, namely sparrow.
Actually the Prolog interpreter finds all the possible proofs for so it also finds THIS and tell us that another possible bird is seagull.

Notice that we can also compute functions in Prolog, since we can look at a function as a relation. For instance fact can be used to represent the relation such that fact(X,Y) holds whenever X is the factorial of Y. The Prolog program for the factorial consists in the fact fact(0,1) and in the clause stating that fact(X,Y) holds if Y is the multiplication of X with the factorial of X-1.