The kind of logic used by Prolog is a subset of First Order Logic called
quantifier-free Horn Clause Logic. As the name suggests, there are no
existential or universal quantifiers. Instead, any variable is implicitly
assumed to be universally quantified. The statement
male(X).
Is
therefore to be taken as [universal]x.male(x), or 'Everything is male'.
Note that any expression which begins with a capital letter or with the
underscore character is a variable in Prolog.
The implication sign ->
or [propersuperset] is represented in Prolog as :-, and the order of
antecedent and consequent is reversed, so p -> q in Prolog will
become q :- p.
Horn Clause logic is characterised by the
fact that it allows only one term in the consequent of a conditional (i.e.
before the :-). What follows the conditional must be a term (possibly
complex and consisting itself of subterms including conjunctions and
disjunctions).
A term p , q is true iff both p and
q are true. A term p ; q is true if p is true or
q is true (or both are).
David Warren, writing in The Art of Prolog
(xi) writes, "The main idea was that deduction could be viewed as a form of
computation, and that a declarative statement of the form:
Q & R
& S -> P
could also be interpreted procedurally, as:
To
solve P, solve Q and R and S."
This is what Prolog does.
Given a
rule such as the following:
mother(M, C):- female(M), parent(M, C).
it
attempts to prove a goal such as:
| ?-mother(liz, chas).
by
first proving female(liz) and then (if this is successful) by proving
parent(liz, chas). If this process fails at any point, Prolog will
report its failure with 'no'.
Note that the deduction algorithm
proceeds in a depth-first, left-to-right order.