Prolog Syntax
Data Domain
atomic values (literals)
• number literals:
e.g., 1994, -34, 3.14159
• symbolic literals:
alphanumeric starting with a lower-case letter or any string enclosed in single
quotes; e.g., dog, xRay, home_run, 'C23', '+*#'
variables (logical variables
that is)
• alphanumeric
starting with an upper-case letter: e.g., C23, NewValue, First_base, or the
“anonymous” variable _
terms (the Prolog
“universe”, inductively defined)
• variables & literals are
(atomic) terms
• a structure name
followed by a parenthesized argument list of other terms is a term, f(t1, t2,
… ,tn), where f is denoted by f/n (f
taking n arguments), and f/1, f/2, ... are all different; the symbolic literals
are the legal structure names
• two terms joined by
an arithmetic operation is a term; e.g., X+1, 2*[1,2,3]
• a finite list of terms — a sequence of terms
enclosed by [,]; e.g., [2, cat, X1]; also, a string written as " … any chars … " is an alias for the list of its ASCII
character codes (integers). For
lists, the notation [hd | tl] is allowed where hd and tl are terms denoting the
head (an element) and tail (another list), respectively.
Formulas & Clauses
atomic formulas — p(t1, t2, … , tn)
n≥0 [when n=0, write just
'p'], where ti (1≤i≤n)
is a term, and p is a symbolic literal called the predicate name; also the usual infix notation for
tests, e.g., X<2
(Horn) clauses — A :- B1, B2, … , Bn.
n≥0 [ for n=0, write A.], where A and Bi (1≤i≤n) are atomic formulas;
A is called the head of the clause and B1, B2, … , Bn the body. If n=0
(i.e., no body), the clause is called a fact (or assertion); if n>0, it is called a conditional
clause (or rule)
program
a Prolog program is a finite
sequence of clauses
comments
there are two forms for comments,
either beginning with '%' and extending to the end of the line, or beginning
with '/*' and extending (over end of lines) to '*/'.
Queries
— ?- B1, B2, … , Bn.
n≥1,
where Bi (1≤i≤n) is an
atomic formula; each Bi is called a goal
Logical Semantics of Prolog
Given a
logic program p, one may pose queries, or goal clauses,
?- B1,
… , Bn. (where each Bi is
an atomic formula called a goal)
which asks
if there exist values (i.e., terms) for the variables for which it can be
inferred from the program p that each of
the formulas Bi is true, and if so,
what are those variable values.
All Prolog
program clauses are “universally quantified” over all variables occurring in a
clause — that is, a clause asserts its truth for all possible values of its
variables.
This is
understood even though no explicit quantification notation is written.
All
queries to a Prolog program are “existentially quantified” over all variables
occurring in a query — that is, a query asks if there exist values of its
variables for which all its goals are true. This quantification is also implicit, not explicit.
The
clauses of a program serve as the axioms of a “theory”, and the Prolog system seeks
to prove whether or not the query is a theorem (i.e., a logical consequence of
the axioms) in this theory.
The
following rules of inference may be applied to resolve queries:
• substitute equal terms for equal
terms;
• if B1, … , Bn are each individually
known to be true assertions, and the conditional assertion A :- B1, … , Bn is known to be
true, then we may conclude that A is true (this is modus ponens);
• if it is known that "X p( … , X, …) is true, then for
any term t we can conclude that p( … , t, …) is true (this is universal instantiation).
• if it is known that p( … , t, …) is true for some term t
we can conclude that
$X p( … , X, …) is true (this is existential
generalization).
Example
The Prolog
program
member(X, [X | Xs]).
member(X, [Y | Xs]) :- member(X, Xs).
is
understood as the set of logical axioms
"X,Xs (member(X, [X | Xs]))
"X,Y,Xs (member(X, Xs) => member(X, [Y |
Xs])).
A Prolog
query such as
?- member(A,[1,2,3]), member(A,[B,3,4]).
is understood as the logical assertion
$A,B
(member(A,[1,2,3]),
member(A,[B,3,4]))
and Prolog can respond with multiple sets of values that
justify the truth of the query
A = 1, B = 1 ;
A = 2, B = 2 ;
A = 3, B = 3 ;
no