Logic Programming

Logic programming is characterized by programming with relations and inference.

Keywords and phrases: Horn clause, Logic programming, inference, modus ponens, modus tollens, logic variable, unification, unifier, most general unifier, occurs-check, backtracking, closed world assumption, meta programming, pattern matching. set, relation, tuple, atom, constant, variable, predicate, functor, arity, term, compound term, ground, nonground, substitution, instance, instantiation, existential quantification, universal quantification, unification, modus ponens, proof tree, goal, resolvent.

A logic program consists of a set of axioms and a goal statement. The rules of inference are applied to determine whether the axioms are sufficient to ensure the truth of the goal statement. The execution of a logic program corresponds to the construction of a proof of the goal statement from the axioms.

In the logic programming model the programmer is responsible for specifying the basic logical relationships and does not specify the manner in which the inference rules are applied. Thus

Logic programming is based on tuples. Predicates are abstractions and generalization of the data type of tuples. Recall, a tuple is an element of

The squaring function for natural numbers may be written as a set of tuples as follows:

Such a set of tuples is called a relation and in this case the tuples define the squaring relation.

Abstracting to the name sqr and generalizing an individual tuple we can define the squaring relation as:

Parameterizing the name gives:

In the logic programming language Prolog this would be written as:

Note that the set of tuples is named sqr and that the parameters are X and Y. Prolog does not evaluate its arguments unless required, so the expression Y is X*X forces the evaluation of X*X and unifies the answer with Y. The Prolog code

may be read in a number of ways; it could be read P where Q or P if Q. In this latter form it is a variant of the first-order predicate calculus known as Horn clause logic. A complete reading of the sqr predicate the point of view of logic is: for every X and Y, Y is the sqr of X if Y is X*X. From the point of view of logic, we say that the variables are universally quantified. Horn clause logic has a particularly simple inference rule which permits its use as a model of computation. This computational paradigm is called Logic programming and deals with relations rather than functions or assignments. It uses facts and rules to represent information and deduction to answer queries. Prolog is the most widely available programming language to implement this computational paradigm.

Relations may be composed. For example, suppose we have the predicates, male(X), siblingof(X,Y), and parentof(Y,Z) which define the obvious relations, then we can define the predicate uncleof(X,Z) which implements the obvious relation as follows:

uncleof(X,Z) <-- male(X), siblingof(X,Y), parentof(Y,Z).

The difference between logic programming and functional programming may be illustrated as follows. The logic program

f(X,Y) <-- Y = X*3+4

which asserts a condition that must hold between the corresponding domain and range elements of the function. In contrast, a functional definition introduces a functional object to which functional operations such as functional composition may be applied.

Logic programming has many application areas:

• Relational Data Bases
• Natural Language Interfaces
• Expert Systems
• Symbolic Equation solving
• Planning
• Prototyping
• Simulation
• Programming Language Implementation

Syntax

Core Prolog

P in Programs
C in Clauses
Q in Queries
A in Atoms
T in Terms
X in Variables

Program ::= Clause... Query | Query
Clause ::= Predicate . | Predicate :- PredicateList .
PredicateList ::= Predicate | PredicateList , Predicate
Predicate ::= Atom | Atom( TermList )
TermList ::= Term | TermList , Term
Term ::= Numeral | Atom | Variable | Structure
Structure ::= Atom ( TermList )
Query ::= ?- PredicateList .
Numeral ::= an integer or real number
Atom ::= string of characters beginning with a lowercase letter or encluded in apostrophes.
Variable ::= string of characters beginning with an uppercase letter or underscore

Terminals = {Numeral, Atom, Variable, :-, ?-, comma, period, left and right parentheses }

While there is no standard syntax for Prolog, most implementations recognize the grammar in Figure M.N. 

---

 

Figure M.N: Prolog grammar

P in Programs C in Clauses Q in Query H in Head B in Body A in Atoms T in Terms X in Variable    P ::= C... Q... C ::= H [ :- B ] . H ::= A [ ( T [,T]... ) ]  B ::= G [, G]...  G ::= A [ ( [ X | T ]... ) ]  T ::= X | A [ ( T... ) ]  Q ::= ?- B .

---

In logic, relations are named by predicate symbols chosen from a prescribed vocabulary. Knowledge about the relations is then expressed by sentences constructed from predicates, connectives, and formulas. An n-ary predicate is constructed from prefixing an n-tuple with an n-ary predicate symbol.

A logic program is a set of axioms, or rules, defining relationships between objects. A computation of a logic program is a deduction of consequences of the program. A program defines a set of consequences, which is its meaning. The art of logic programming is constructing concise and elegant programs that have the desired meaning.

The basic constructs of logic programming, terms and statements are inherited from logic. There are three basic statements: facts, rules and queries. There is a single data structure: the logical term.

Facts, Predicates and Atoms

father(bill,mary).
plus(2,3,5).
...

Queries

?- father(bill,mary).
?- father(bill,jim).

Semantics

There is a close relation between the axiomatic semantics of imperative programs and logic programs. A logic program to sum the elements of a list could be written as follows.

sum([Nth],Nth).
sum([Ith|Rest],Ith + Sum_Rest) <-- sum(Rest,Sum_Rest).

A[N] = sum_{i=N}^N A[i]}
sum([A[N]],A[N]).
sum_{i=I}^N A[i] = A[I] + S if 0 < I, sum_{i=I+1}^N A[i] = S}
sum([A[I],...,A[N]], A[I]+S) <--  sum([A[I+1],...,A[N]],S).

Operational Semantics

• Logic Program A logic program is a finite set of facts and rules.
• Interpretation and meaning of logic programs.

The rule of instantiation (P(X) deduce P(c)). The rule of deduction is modus ponens. From A :- B1, B2, ..., Bn. and B1', B2', ..., Bn' infer A'. Primes indicate instances of the corresponding term.

The meaning M(P) of a logical program P is the set of unit goals deducible from the program.

A program P is correct with respect to some intended meaning M iff the meaning of P M(P) is a subset of M (the program does not say things that were not intended).

A program P is complete with respect to some intended meaning M iff M is a subset of M(P) (the program says everything that was intended).

A program P is correct and complete with respect to some intended meaning M iff M = M(P).

a.
b <--  a.
b?

parent_of(a,b).
parent_of(b,c).
ancestor_of(Anc,Desc) <-- parent_of(Anc,Desc).
ancestor_of(Anc,Desc) <-- parent_of(Anc,Interm) \wedge
   ancestor_of(Interm,Desc).
parent_of(a,b)?
ancestor_of(a,b)?
ancestor_of(a,c)?
ancestor_of(X,Y)?

Definition M.N:

A unifier of two terms is a substitution making the terms identical. If two terms have a unifier, we say they unify.

For example, two identical terms unify with the identity substitution. concat([1,2,3],[3,4],List) and concat([X|Xs],Ys,[X|Zs]) unify with the substitutions {X = 1, Xs = [2,3], Ys = [3,4], List = [1|Zs]}

There is just one rule of inference which is resolution. Resolution is much like proof by contradiction. An instance of a relation is ``computed'' by constructing a refutation. During the course of the proof, a tree is constructed with the statement to be proved at the root. When we construct proofs we will use the symbol ¬ to mark formulas which we either assume are false or infer are false and the symbol [] for contradiction. Resolution is based on the inference rule modus tollens and unification. This is the modus tollens inference rule.

From  ¬ B
and  B <-- A0,...,An
infer ¬ A0 or...or ¬ An

1  From   ¬ B
2  and   A0
3  and   B <-- A0,A_{1}
4  infer   ¬ A0   or}  ¬ A_{1}
5  choose   ¬ A0
6  contradiction   []
7  choose   ¬ A_{1}
8  no further possibilities}  open}

As an example of computing in this system of logic suppose we have defined the relations parent and ancestor as follows:

1.  parent_of(ogden,anthony)
2.  parent_of(anthony,mikko)
3.  parent_of(anthony,andra)
4.  ancestor_of(A,D) <-- parent_of(A,D) 
5.  ancestor_of(A,D) <-- parent_of(A,X) 
6.  ancestor_of(X,D)

    ¬ ancestor(ogden,mikko)  the assumption
    ¬ parent(ogden,X)  or}  ¬ ancestor(X,mikko)
         resolution}
    ¬ parent(ogden,X)  first choice 
    ¬ parent(ogden,anthony)  unification with first entry 
    []  produces a contradiction
    ¬ ancestor(anthony,mikko)  second choice
    ¬ parent(anthony,mikko)  resolution
    []  A contradiction of a
      fact.}

UNIVERSAL QUANTIFICATION, EXISTENTIAL QUANTIFICATION

The unification algorithm can be defined in Prolog. Figure~\ref{lp:unify} contains a formal definition of unification in Prolog
 

• single assignment
• parameter passing
• record allocation
• read/write-once field-access in records

\begin{array}{l}
\frac{A1 <-- B.},  ?- A1, A2,...,An.}}{?- B, A2,...,An.}} 

\frac{?- true, A1, A2,...,An.}}{?- A1, A2,...,An.}} 
\caption{Inference Rules\label{lp:ir}}

a <-- b \wedge c . b <-- d . b <-- e . ?- a .

?- b \wedge c . ?- d \wedge c . ?- e \wedge c. ?- c. ?-

Inference and Unification

R = (A :- B1,...,Bn) and
B'1.
...
B'n.

Definition: A logic program is a finite set of rules.

Definition: An existentially quantified goal G is a logical consequence of a program P iff there is a clause in P with an instance A :- B1,...,Bn, n \geq 0 such that B1,...,Bn are logical consequences of P and A is an instance of G.

The control portion of the the equation is provide by an inference engine whose role is to derive theorems based on the set of axioms provided by the programmer. The inference engine uses the operations of resolution and unification to construct proofs.

Resolution says that given the axioms

f if a0, ..., a_m.

g if f, b0, ..., bn.

g if a0, ..., a_m, b0, ..., bn.

Unification is the binding of variables. For example

A query containing a variable asks whether there is a value for the variable that makes the query a logical consequence of the program.

?- father(bill,X).
?- father(X,mary).
?- father(X,Y).

Definition: Constants and variables are terms. A compound term is comprised of a functor and a sequence of terms. A functor is characterized by its name, which is an atom and its arity, or number of arguments.

X, 3, mary, fatherof(F,mary), ...

Definition: A substitution is a finite set (possibly empty) of pairs of the form Xi=ti, where Xi is a variable and ti is a term, and Xi\neq Xj for every i \neq j, and Xi does not occur in tj, for any i and j.

p(a,X,t(Z)), p(Y,m,Q); theta = { X=m,Y=a,Q=t(Z) }

Definition: Two terms A and B are said to have a common instance C iff there are substitutions theta1 and theta2 such that C = Atheta1 and C = Btheta2.

A = plus(0,3,Y), B = plus(0,X,X). C = plus(0,3,3)
since C = A{ Y=3} and C = B{ X=3}.

p(a,X,t(Z))theta = p(Y,m,Q)theta where theta = { X=m,Y=a,Q=t(Z) }

unify(A,B) :- unify1(A,B).

unify1(X,Y) :- X == Y.
unify1(X,Y) :- var(X), var(Y), X=Y. % The substitution
unify1(X,Y) :- var(X), nonvar(Y), \+ occurs(X,Y), X=Y. % The substitution
unify1(X,Y) :- var(Y), nonvar(X), \+ occurs(Y,X), Y=X. % The substitution
unify1(X,Y) :- nonvar(X), nonvar(Y), functor(X,F,N), functor(Y,F,N),
X =..[F|R], Y =..[F|T], match_list(R,T).

match_list([],[]).
match_list([X|R],[H|T]) :- unify(X,H), match_list(R,T).

occurs(A,B) :- A == B.
occurs(A,B) :- nonvar(B), functor(B,F,N), occurs(A,B,N).

occurs(A,B,N) :- N > 0, arg(N,B,AN), occurs(A,AN),!. % RED
occurs(A,B,M) :- M > 0, N is M - 1, occurs(A,B,N).

A Simple Interpreter for Pure Prolog

Figure M.N: A simple interpreter for pure Prolog

is_true( Goals ) <-- resolved( Goals ).
is_true( Goals ) <-- write( no ), nl.

resolved([]).
resolved(Goals) <-- select(Goal,Goals,RestofGoals),
                       % Goal unifies with head of some rule 
                       clause(Head,Body), unify( Goal, Head ),
                       add(Body,RestofGoals,NewGoals),
                       resolved(NewGoals).

prove(true).
prove((A,B)) <-- prove(A), prove(B). % select first goal
prove(A) <-- clause(A,B), prove(B). % select only goal and find a rule

is the Prolog code for an interpreter.

The interpreter can be used as the starting point for the construction of a debugger for Prolog programs and a starting point for the construction of an inference engine for an expert system.

The operational semantics for Prolog are given in Figure~\ref{lp:opsem}

Logic Programming (Horn Clause Logic) -- Operational Semantics
Abstract Syntax:

   P in Programs
   C in Clauses
   Q in Queries
   T in Terms
   A in Atoms
   X in Variables 

P ::= (C | Q)...
C ::= G [ <-- G_{1} [ \wedge G_{2}]...] . 
G ::= A [ ( T [,T]... ) ] 
T ::=  X | A [ ( T [,T]... ) ] 
Q ::= G [,G]... ?

Semantic Domains:

   beta in  {\bf B} = Bindings
   \epsilon in  {\bf E} = Environment

Semantic Functions: 

   R in Q} --> B} -->  B } + (B} × }yes }) + } no } }
   U in C } × C } --> B } --> B }

Semantic Equations: 

R[ ?} ] beta , \epsilon &=&  (beta, yes})
R[ G ] beta , \epsilon &=&  beta'
&  where }
&&G' in \epsilon ,   U [ G, G' ] beta = beta'
R[ G ] beta , \epsilon &=& R[ B ] beta' , \epsilon &  where }
&&(G' <-- B) in \epsilon ,   U [ G, G' ] beta = beta'
R[ G1,G2 ] beta , \epsilon &=& R[ B,G2 ] ( R [ G1 ] beta , \epsilon ), \epsilon
R[ G } ] beta , \epsilon &=&  no }
&  where no other rule applies}

\caption{Operational semantics\label{lp:opsem}}

Declarative Semantics

Definition M.N:

Let P be a logic program. The Herbrand universe of P, denoted by U(P) is the set of ground terms that can be formed from the constants and function symbols appearing in P

Definition M.N:

The Herbrand base, denoted by {\cal B}(P), is the set of all ground goals that can be formed from the predicates in P and the terms in the Herbrand universe.

The Herbrand base is infinite if the Herbrand universe is.

Definition M.N:

An interpretation for a logic program is a subset of the Herbrand base.

An interpretation assigns truth and falsity to the elements of the Herbrand base. A goal in the Herbrand base is true with respect to an interpretation if it is a member of it, false otherwise.

Definition M.N:

An interpretation I is a model for a logic program if for each ground instance of a clause in the program A <-- B1, ... , Bn A is in I if B1, ... , Bn are in I.

This approach to the semantics is often called the term model.

Denotational Semantics

Pragmatics

Logic Programming and Software Engineering

• obtain a problem description
• define the intended model of interpretation (domains, symbols etc)
• devise a suitable theory (the logic component) suitably restricted so as to have an efficient proof procedure.
• describe the control component of the program
• use declarative debugging to isolate errors in definitions

• Pro
• Closer to problem domain thus higher programmer productivity
• Separation of logic and control (focuses on the logical structure of the problem rather than control of execution)
• Simple declarative semantics and referential transparency
• Suitable for prototyping and exploratory programming
• Strong support for meta-programming
• Transparent support for parallel execution
• Con
• Operational implementation is not faithful to the declarative semantics
• Unsuited for state based programming
• Often inefficient

The Logical Variable

Here is a definition of the relation between the prefix and suffixes of a list. The relation is named concat because it may be viewed as defining the result of appending two lists to get the third list.

{l} concat([ ],[ ]) concat([H|T],L,[H|TL]) <-- concat(T,L,TL)

Logical variables operate in a way much different than variables in traditional programming languages. By way of illustration, consider the following instances of the concat relation.

1. ?- concat([a,b,c],[d,e],L). L = [a, b, c, d, e] the expected use of the concat operation.
2. ?- concat([a,b,c],S,[a,b,c,d,e]). S = [d, e] the suffix of L.
3. ?- concat(P,[d,e],[a,b,c,d,e]). P = [a, b, c] the prefix of L.
4. ?- concat(P,S,[a,b,c,d,e]). P = [ ], S = [a,b,c,d,e] P = [a], S = [b,c,d,e] P = [a,b], S = [c,d,e] P = [a,b,c], S = [d,e] P = [a,b,c,d], S = [e] P = [a,b,c,d,e], S = [ ] the prefixes and sufixes of L.
5. ?- concat(_,[c|_],[a,b,c,d,e]). answers Yes since c is the first element of some suffix of L.

concat(L1,L2,L)
prefix(Pre,L) <-- concat(Pre,_,L).
sufix(Suf,L) <-- concat(_,Suf,L).
split(L,Pre,Suf) <-- concat(Pre,Suf,L).
member(X,L) <-- concat(_,[X|_],L).

There two simple types of constants, string and numeric. Arrays may be represented as a relation. For example, the two dimensional matrix

may be written as {ll} data(1,1,mary)&data(1,2,18.47) data(2,1,john)&data(2,2,34.6) data(3,1,jane)&data(3,2,64.4)

Records may be represented as terms and the fields accessed through pattern matching.

book(author( last(aaby), first(anthony), mi(a)),
   title('programming language concepts),
   pub(wadsworth),
   date(1991))

book(A,T,pub(W),D)

Lists may be used to simulate stacks, queues and trees. In addition, the logical variable may be used to implement incomplete data structures.

Incomplete Data Structures

lookup(Key,Data,bt(Key,Data,LT,RT)) 
lookup(Key,Data,bt(Key0,Data0,LT,RT)) <-- Key @< Key0,
   lookup(Key,Data,LT) 
lookup(Key,Data,bt(Key0,Data0,LT,RT)) <-- Key @> Key0,
   lookup(Key,Data,RT)

lookup(john,46,BT), lookup(jane,35,BT), lookup(allen,49,BT), lookup(jane,Age,BT).

The logical and the incomplete data structure can be used to append lists in constant time. The programming technique is known as difference lists. The empty difference list is X/X. The concat relation for difference lists is defined as follows:

concat_dl(Xs/Ys, Ys/Zs, Xs/Zs)

?- concat_dl([1,2,3|X]/X,[4,5,6|Y]/Y,Z).
 
   _X = [4,5,6 | 11]
   _Y = 11
   _Z = [1,2,3,4,5,6 | 11] / 11
Yes

ol_dl([ ],X/X) <-- var(X)
ol_dl([F|R],[F|DL]/Y) <-- ol_dl(R,DL/Y)

Arithmetic

times(X,Y,X×Y)

times(X,Y,Z) <-- Z is X×Y

Iteration vs Recursion

 n! = 1 if n = 0
      n× (n-1)! if n > 0

factorial(0,1)
factorial(N,N×F) <-- factorial(N-1,F)

factorial(0,1)
factorial(N,F)<-- M is N-1, factorial(M,Fm), F is N×Fm

fac(N,F) <-- fac(N,1,F)
fac(0,F,F)
fac(N,P,F) <-- NP is N×P, M is N-1, fac(M,NP,F)

As a further example of the relation between recursive and iterative definitions, here is a recursive version of the relation between a list and its reverse.

reverse([ ],[ ])
reverse([H|T],R) <-- reverse(T,Tr), concat(Tr,[H],R)

rev(L,R)<-- rev(L,[ ],R)
rev([ ],R,R)
rev([H|T],L,R) <-- rev(T,[H|L],R)

Backtracking

Exceptions

Logic Programming vs Functional Programming

Prolog and Logic

The Logic of Prolog

Horn Clauses

• A <--> B with A --> B and B --> A
• A --> B with not A \/ B
• Move negations inward (from the outside inward). Replace
• not (A and B) with not A or not B
• not (A or B) with not A and not B
• not Exists x. P with Forall x. not P
• not Forall x. P with Exists x. not P
• Skolemize (replace existential variables with skolem constants or skolem fuctions of universal variables (from the outside inward). Replace
• Exists x. P(x) with P(c) where c is new
• Forall x. ... Exists y. P(y) with Forall x. ... P(f_c(c_k)) where f_c and c_k are new
• Move universal quantifiers outward. Replace

... Forall x.P(x) with Forall x. ... P(x)
(we can just drop the quantifiers)
• Put quantifier free portion into conjunctive normal form (conjunction of disjunctions). Replace
• (A and B) or C with (A or C) and (B or C)
• (A and C) or (B and C) with (A or B) and C
(move conjunctions out and disjunctions in)

• If m=0 and n=1 then we have a Prolog fact.
• If m>0 and n=1 then we have a Prolog rule.
• If m>0 and n=0 then we have a Prolog query.

Resolution and unification, forward and backward chaining

If Aj and B_y `match' then by resolution: ...not Ai \/ not Aj \/ B_k...
...not A_x \/ B_y \/ B_z...
----------------------------
...not Ai \/...\/ A_x \/ B_z...\/ B_k
Matching is called unification.

Direction of Proof

• Forward chaining: proofs proceed from facts through rules to conclusions (goals). Also called bottom-up.
• Backward chaining: proofs proceed from goals back through rules toward facts. Also called top-down and goal-directed.

The Illogic of Prolog

Prolog is not logic programming. The execution model for Prolog omits the occurs check, searches the rules sequentially, and selects goals sequentially. Backtracking, infinite search trees ...

As in functional programming, lists are an important data structure logic programming. The empty list is represented by [ ], a list of n elements by [X1, ... , Xn] and the first i elements of a list and the rest of the list by [X1,...,Xi|R]. In addition, data structures of arbitrary complexity may be constructed from the terms.

• Depth-first, left-right search instead of breadth-first parallel search means that rule and clause order can matter. Instead of combinatorial explosion in the size of the search tree, we may have infinite recursion.
• There is no `occurs check' when performing unification. This means that X unifies with f(X) -- infinite terms may be constructed during unification. Since this is an infrequent occurrence, we are trading correctness for reduction in running time.
• Negation by failure, `not'. Closed world assumption. Horn clause logic does not include the `not' operator, however its use simplifies programs.
• The `cut', prunes unnecessary branches. Encourages a `goto' style programming.

Incompleteness

p( a, b ).
p( c, b ).
p( X, Z ) <-- p( X, Y ), p( Y, Z).
p( X, Y ) <-- p( Y, X ).
?- p( a, c ).

Unfairness

concat( [ ], L, L ).
concat( [H|L1], L2, [X|L] ) <-- concat( L1, L2, L ).
concat3( L1, L2, L3, L ) <-- concat( L1, L2, L12 ),
   concat( L12, L3 L ).
?- concat3( X, Y, [2], L).

Unsoundness

test <-- p( X, X ).
p( Y, f( Y )).
?- test.

The execution of this logic program results in the construction of an infinite data structure.

concat( [ ], L, L ).
concat( [H|L1], L2, [X|L] ) <-- concat( L1, L2, L ).
?- concat( [ ], L, [1|L] ).

Negation

p( a ).
r( b ) <-- not p( Y ).
?- not p(b).

q( a ) <-- r( a ).
q( a ) <-- not r( a ).
r( X ) <-- r( f( X ) ).
?- q ( a ).

Control Information

a(1).
a(2).
a(3).
p <-- a(I),!,print(I),nl,fail.
?- p.
1
 
No

Extralogical Features

Some other extralogical primitives include bagof, setof, assert, retract, univ. These are outside the scope of first-order logic.

Input and output introduce side effects.

The extralogical primitives \verb+bagof+, \verb+setof+, \verb+assert+, and \verb+retract+ are outside the scope of first-order logic but are useful from the pragmatic point of view.

In Prolog there are builtin predicates to test for the various syntactic types, lists, numbers, atoms, clauses. Some predicates which are commonly available are the following.

{ll} var(X)&X is a variable atomic(A)&A is an atom or a numeric constant functor(P,F,N)&P is an N-ary predicate with functor F clause(Head,Body)&Head <-- Body is a formula. L =..List, call(C), assert(C), retract(C), bagof(X,P,B), setof(X,P,B)

Figure M.N:

trace(Q) <-- trace1([Q])
trace1([])
trace1([true|R]) <-- !, trace1(R).
trace1([fail|R]) <-- !, print('< '), print(fail), nl, fail.
trace1([B|R]) <-- B =..[','|BL], !, concat(BL,R,NR), trace1(NR).

trace1([F|R]) <-- builtin(F),
      print('> '), print([F|R]), nl,
      F,
      trace1(R),
      print('< '), print(F), nl

trace1([F|R]) <-- clause(F,B),
      print('> '), print([F|R]),nl,
      trace1([B|R]),
      print('< '), print(F), nl

trace1([F|R]) <--  \+ builtin(F), \+ clause(F,B),
      print('> '), print([F|R]),nl,
      print('< '), print(F), print(' '), print(fail), nl, fail

\caption{Program tracer for Prolog\label{lp:trace}}

contains an example of meta programming. The code implements a facility for tracing the execution of a Prolog program. To trace a Prolog program, instead of entering {\tt ?- P.} enter {\tt ?- trace(P).}

Multidirectionality

Rule Order

concat([ ],L,L).
concat([H|T],L,[H|R]) <-- concat(T,L,R).
?- concat(L1,[2],L).

L1 = [ ], L = [2] 
L1 = [V1], L = [V1,2] 
L1 = [V1,V2], L = [V1,V2,2] 
...

append([H|T],L,[H|R]) :- append(T,L,R).
append([ ],L,L).
?- append(L1,[2],L).

Historical Perspectives and Further Reading

• Intuitionistic mathematics and proof theory.
• Literal normal form, conjunctive normal form and Horn Clause Logic
• Robinson's unification algorithm and the resolution principle. Two terms are said to be unifiable iff there is are substitutions which applied to each makes them the same.
• Kowalski normal form -- Kowalski
• Definite clause grammars -- Colmerauer
• Relational Data Bases -- Codd

Relations and the Relational Algebra
DataLog
• Prolog -- Colmerauer, Warren (David)

• Aristotle: (384-322 BCE) -- Theory of syllogistic
• Liebniz (1646-1716): De Arte Combinatoriua 1666 -- calculus of reasoning
• Boole: 1854 -- Boolean logic
• Frege: 1879 Begriffsschrift -- separation of logic from mathematics
• Russell, B, & Whitehead, A. N.: 1910-13 -- Logicism (reduction of mathematics to logic)
• Hilbert, David: 1900 -- Formalism (finitary proofs of consistency)
• Brouwer, L.E.J.: (1881-1966) -- Intuitionism (mathematical certitude is in intuition & explicit construction)
• Gödel, Kurt: 1933 -- incompleteness theorem
• Tarski, Alfred: 1936 -- separation of logic and models
• Church, Alonso: 1936 -- non-termination of proof algorithm for non-theorems
• Robinson, J. Alan: 1965 -- resolution principle
• Kowalski, Robert: 1974 -- predicate logic as a programming language
• Tärnlund, S-A: 1977 -- Horn clause computability
• Pereira, Fernando: -- implementation of Prolog
• Warren, David: -- implementation of Prolog, Warren abstract machine (WAM)
• Classical logic (propositional, predicate/first-order )
• Other logics: Fuzzy, non-monotonic

• Improved implementations: the Gödel programming language
• Combination of logic and functional paradigms: the Escher programming language

Clocksin & Mellish, Programming in Prolog 4th ed. Springer-Verlag 1994.

Hill, P. & Lloyd, J. W., The Gödel Programming Language MIT Press 1994.

Hogger, C. J., Introduction to Logic Programming Academic Press 1984.

Lloyd, J. W., Foundations of Logic Programming 2nd ed. Springer-Verlag 1987.

Nerode, A. & Shore, R. A., Logic for Applications Springer-Verlag 1993.

Robinson, J. A., Logic: Form and Function North-Holland 1979.

Exercises

1. Modify concat to include an explicit occurs check.
2. Construct a Prolog based family database. Include the following relations: parentof, grandparentof, ancestorof, uncleof, auntof, and any others of your choice.
3. The relational algebra is ... query languages of relational database management systems is another approach to the logic model.

The fundamental entity in a relational database is a relation which is viewed as a table of rows and columns, where each row, called a tuple, is an object and each column is an attribute or propery of the object.

A database consists of one or more relations. The data stored in the relations is manipulated using commands written in a query language. The operations provided the query language include union, set difference, cartesian product, projection, and selection. The first-order predicate logic can be used to represent knowledge and as a language for expressing operations on relations. -- Ullman (Principles of Database and Knowledge-base Systems) CSP 1988.

• The tables of a relational database are represented as Prolog facts.
• The Relational algebra implemented via Prolog rules and queries.
• Selection:

select( variables ) :- conditions on the constants.
Constants select rows in the relation.
• Intersection:

r_1_in_r₂( Vars ) :- r_1( Vars ), r₂( Vars ).
selects the entities that are in both r_1 and r₂ (use the same variables).
• Difference:

diff_r_1_r₂( Vars ) :- r_1( Vars ), not r₂( Vars ).
selects the entities in r_1 that are not in r₂.
• Projection:

pr( variables ) :- r( variables and don't cares ).
Don't cares represent columns to be deleted.
• Cartesian product:

prod( variables ) :- r_1( vars ), r₂( vars ).
prod variables is the list of variables both in r_1 and r₂.
• Union: (two rules are required to perform union.)

union( variables ) :- first_relation( variables ).
union( variables ) :- second_relation( variables ).

• Natural Join: In the rule,

nat_join( variables shared variables ) :- 
    r_1(variables, shared variables), 
    r2(variables, shared variables).


the shared variables restrict search to common elements, reduced number of variables in the join eliminate multiple columns.
4. Construct a family data base f_db(f,m,c,sex) and define the following relations, f_of, m_of, son_of, dau_of, gf, gm, aunt, uncle, ancestor, half_sis, half_bro.
5. Business Data base
6. Blocks World
7. CS Degree requirements; course(dept,name,prereq). don't forget w1 and w2 requirements.
8. Circuit analysis
9. Tail recursion
10. Compiler
11. Interpreter
12. Tic-Tac-Toe
13. DCG
14. Construct Prolog analogues of the relational operators for union, set difference, cartesian product, projection and selection.
15. Airline reservation system

Objective:

• Atoms and Terms
• Relations, predicates and facts
• Queries
• Terms, logical variable, substitutions, instances
• Unification and the MGU
• Variables and Quantification
• Rules
• Inference
• Abstract Interpreter for Logic Programs
• The Meaning of Logic Programs

The logical variable, substitutions and instances

Rules

          
A :- B1, B2, ..., Bn.

ancestor(X,Y) :- father(X,Y).
ancestor(X,Z) :- father(X,Y), ancestor(Y,Z).

father(bill,jim).
father(jim,jane).
?- father(bill,Y), father(Y,jane).

For A1,...,An and theta
A1theta,...,Antheta each is deducible.

Quantifiers

father(adam,X).

father(bill,jim).
father(jim,jane).
?- father(bill,Y), father(Y,jane).

For A1,...,An and theta
A1theta,...,Antheta each is deducible.