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