Admin U

NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

Exam in December is only for students visiting Edinburgh for

1 semester.
Dates of exams are now known. These are provisional,
check for confirmed dates later.
There is an on-line programming exam;
and a short (1 hour) theory exam.

Alan Smaill Logic Programming Nov 2. 2015 1/32

 Today U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

Predicate Calculus: syntax, semantics

Definite Clause logic
Substitutions and Unification
Inference System of definite clause logic

Alan Smaill Logic Programming Nov 2. 2015 2/32

 Recall: propositional definite clauses U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

We saw use of propositional definite clauses for reasoning:

Notion of logical consequence via interpretations;
Notion of an inference system for proofs;
Notion of proof search.

We have similar notions for the language of pure Prolog.

Alan Smaill Logic Programming Nov 2. 2015 3/32

 Properties U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

Correctness of Prolog proof search: straightforward, see later

F1 , . . . , Fn `Prolog g1 ∧ · · · ∧ gm implies F1 , . . . , Fn ` g1 ∧ · · · ∧ gm

Soundness of Inference System: not so hard, see later

F1 , . . . , Fn ` g1 ∧ · · · ∧ gm implies F1 , . . . , Fn |= g1 ∧ · · · ∧ gm

Completeness of Inference System: propositional case argued last

time
F1 , . . . , Fn |= g1 ∧ · · · ∧ gm implies F1 , . . . , Fn ` g1 ∧ · · · ∧ gm

Incompleteness of Prolog proof search:

take easy example
F1 , . . . , Fn ` g1 ∧ · · · ∧ gm does not imply
F1 , . . . , Fn `Prolog g1 ∧ · · · ∧ gm

Alan Smaill Logic Programming Nov 2. 2015 4/32

 Predicate Calculus U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

Logic Programming aims to use Predicate Calculus as a

representation language, where programs have a declarative
reading as logical theories – ie as sets of formulas of the Predicate
Calculus. The main computation follows from searching for a
derivation of a query from the theory. The slogan is:
A program is a theory over a formal logic, and its
computation is deduction in that theory.
To make this idea work effectively, a subset of predicate logic is
taken.

Alan Smaill Logic Programming Nov 2. 2015 5/32

 Grammar for first-order logic U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

. . . aka predicate calculus

Define terms by

term ::= constant

| var
| fn symbol ( term list )
term list ::= term
| term , term list

Alan Smaill Logic Programming Nov 2. 2015 6/32

 Formulas (= making a statement) U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

form ::= pred ( term list )

| ¬ form
| form ∨ form
| form ∧ form
| form → form
| ∀ var form
| ∃ var form

Use precedence to disambiguate (or brackets).

Alan Smaill Logic Programming Nov 2. 2015 7/32

 Syntax and disambiguation in Prolog U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

The syntax of Prolog does not distinguish between function

symbols and predicates – but it is important when looking at the
declarative reading of the language to make this distinction.
Prolog allows functors (ie predicates and function symbols) to be
declared is infix. It allows the use of brackets to impose a reading,
and also has a system of precedence that allows brackets to be
omitted while imposing a unique reading of a statement.
To check on the parsing in (sicstus, and maybe other) Prolog, use
display/1:

| ?- display(a + b * c = 4).
=(+(a,*(b,c)),4)
yes

Alan Smaill Logic Programming Nov 2. 2015 8/32

 Semantics U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

We say what it is for a formula to be true under an interpretation

in a structure.
Write S for a structure together with an associated interpretation
I.
Given S, and a formula F, write S |= F for “F is true in S”.

Alan Smaill Logic Programming Nov 2. 2015 9/32

 Modelling the world U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

We suppose that the world can be describe in terms of

set of objects
functions
relations
where
functions map objects to objects
relations with n arguments describe properties of n objects.

Alan Smaill Logic Programming Nov 2. 2015 10/32

 Example U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

Look at a blocks world:

d
c
a b

base

This can be described using objects O = {base, a, b, c, d, e}.

We can say which object is on which other one with a 2-place
relation, on:
on = {(e, c), (c, a), (e, d), (d, b), (b, base), (a, base)}.

Alan Smaill Logic Programming Nov 2. 2015 11/32

 Structures U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

A structure is a set with some functions and relations.

We interpret a formula by giving an interpretation mapping:
constants to objects
function symbols to functions
predicate symbols to relations.

Alan Smaill Logic Programming Nov 2. 2015 12/32

 Example U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

For the blocks world, fix the language:

Constants: base, a, b, c, d, e.
Function symbol: next
Predicate: on
An interpretation for this is:

I ( base ) = base I( a ) = a
I( b ) = b I ( on ) = on
..
.

We could take I ( base ) = a however.

Alan Smaill Logic Programming Nov 2. 2015 13/32

 Satisfaction U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

We now say what it is for a formula to be true under an

interpretation in a structure. Write S for a structure together with
an associated interpretation I.
Given S, and a formula F, write “F is true in S” as:

S |= F

Suppose P is a predicate and c is a constant. To see if

S |= P(c)

look at I ( P ) and I ( c ):

S |= P(c) iff I( P )(I( c )).

Alan Smaill Logic Programming Nov 2. 2015 14/32

 Satisfaction ctd U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

Extend this to formulas with connectives:

S |= A ∧ B iff S |= A and S |= B
S |= A ∨ B iff S |= A or S |= B
S |= A → B iff ( not (S |= A)) or S |= B
S |= ¬A iff not (S |= A)

For example, with interpretation given,

B |= on(c, a) ∧ on(e, c)
B |= ¬(on(c, a) → on(e, a))
not(B |= on(a, c) ∨ on(c, c))

Alan Smaill Logic Programming Nov 2. 2015 15/32

 Quantifiers U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

Roughly, the idea is that for any statement Φ(v ) which talks about
variable v :

S |= ∀vn (Φ(vn )) if and only if S |= Φ(vn )

for all interpretations of vn

S |= ∃vn (Φ(vn )) if and only if S |= Φ(vn )

for some interpretation of vn

Alan Smaill Logic Programming Nov 2. 2015 16/32

 Logical Consequence U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

Our semantics gives us a notion of logical consequence as before.

We say that a formula G is a logical consequence of formulae
F1 , F2 . . . Fn (meaning that it follows logically) if and only if, for
all structures with interpretation S,

if S |= F1 and . . . and S |= Fn ,
then S |= G.

When this is true, we write

F1 , F2 . . . Fn |= G.

Alan Smaill Logic Programming Nov 2. 2015 17/32

 Definite Clause Logic U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

Suppose we restrict the statements we consider as follows:

Drop quantifiers (but keep variables)
Drop ¬ ∨ (but keep ∧, →).
Only allow formulas of the shape

p(t1 , . . . , tn )

for some predicate p (ie an atomic statement), or

A1 ∧ · · · ∧ An → B

where each Ai is an atomic statement.

Alan Smaill Logic Programming Nov 2. 2015 18/32

 Definite Clauses ctd U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

Formulas of these shapes are called Definite Clauses, and they

have interesting properties for inference.
We can use our previous definition of logical consequence here; for
statements involving variables, take the statement to be implicitly
universally quantified.

The idea is that if knowledge can be expressed as a set of definite

clauses S, and we are interested in knowing if some atomic
statements follow, then we want to find out if

S |= A1 ∧ . . . An .

where variables in the query are implicitly existentially quantified.

Alan Smaill Logic Programming Nov 2. 2015 19/32

 Example U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

Take definite clauses as follows.

father (jon, kay )

daughter (kay , liz)
father (X , Y ) → ancestor (X , Y )
daughter (X , Y ) → ancestor (Y , X )
ancestor (X , Y ) ∧ ancestor (Y , Z ) → ancestor (X , Z )

Then we can ask if it follows that ancestor (jon, liz), or if there is a

Q such that ancestor (Q, kay ): ∃q.ancestor (q, kay ).

Alan Smaill Logic Programming Nov 2. 2015 20/32

 Substitution U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

A substitution is formally as an association of terms for variables,

ie a set of variable/term pairs. Thus { x/a, y/g(w), z/b } is the
substitution where the variable x is to be replaced by the term a,
the variable y is to be replaced by the term g(w), and so on.
A substitution is applied by replacing free occurrences of the
variables by the corresponding terms. For a substitution S and a
formula F we write FS for the result of applying the substitution.
For the substitution above, we have for example

P(x, g(x), y){ x/a, y/g(w), z/b } = P(a, g(a), g(w))

Alan Smaill Logic Programming Nov 2. 2015 21/32

 Substitution ctd U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

Substitutions are important, since the result of a successful logic

program query is a substitution that associates a term with each of
the (Prolog) variables that appear in the initial query. We will see
how this substitution is characterised and computed.

Note that the substitutions for variables in S must be applied

simultaneously, rather than one at a time.
Consider { x/y , y /g (a) } applied to f (x); the result is f (y ), and
not f (g (a)) which we would get by applying first the substitution
{ x/y } and then { y /g (a) }.

Alan Smaill Logic Programming Nov 2. 2015 22/32

 Substitution ctd U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

We will want to combine substitutions into a single substitution to

compute the result of a query. Write S1 o S2 for the substitution
that applies S1 first, and then S2 . The defining property of this
composition operation is that it is always true that

t(S1 o S2 ) = (tS1 )S2

The identity substitution { } leaves terms untouched ( t{ } = t).

So S o{ } = S = { } o S.
Substitutions are just function applications, so we also always have

t(S1 o(S2 o S3 )) = t((S1 o S2 ) o S3 )

ie S1 o(S2 o S3 )) = ((S1 o S2 ) o S3 ).

Alan Smaill Logic Programming Nov 2. 2015 23/32

 Unification U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

We can now define what it is for two expressions to be unifiable.

This occurs for formulae F, G when there is a substitution θ such
that Fθ = Gθ. We can think of this as saying that there are values
for the variables that make the equation true (by making the terms
identical). In this case, θ is said to be the unifier of the two
expressions. In logic programming, unifiers are the basic objects to
be computed during program execution.
We can define an order relation between substitutions:
when is one substitution more general than another? Define
S1 4 S2 to mean that there is a third substitution S such that
S1 = S2 o S. We say that S2 is more general than S1 .
Thus { x/f (a), y /g (a, f (b)), w /f (b) } 4 { x/f (z), y /g (z, w ) }
– what is the S here?

Alan Smaill Logic Programming Nov 2. 2015 24/32

 Most general unifiers U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

It turns out that in the case of the term syntax we have given, if
two terms t1 , t2 are unifiable, then there is a most general unifier
(mgu) S. This means that
1. t1 S = t2 S
2. for any S 0 , if t1 S 0 = t2 S 0 , then S 0 4 S.
The most general unifier is not unique as a substitution; however,
any two mgus are equivalent in the following sense
If S1 , S2 are mgus for t1 , t2 , then S1 4 S2 and S2 4 S1 .
This last property in fact just means that t1 S1 , t1 S2 just differ by
renaming of variables back and forth.

Alan Smaill Logic Programming Nov 2. 2015 25/32

 Inference System for Definite Clause Logic U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

The given definite clauses are taken as axioms. We use a single

inference rule, Backchain:

p1 θ, p2 θ, . . . , pn θ, (p1 ∧ p2 ∧ . . . ∧ pn ⇒ q)
where θ is mgu of q 0 , q
q0θ

Given a query (∃X )r (x), see if r (X ) unifies with the “head”

formula of a definite clause, with unifier θ. If so, top-down search
will look for justifications of p1 θ, p2 θ, . . . , pn θ.

Alan Smaill Logic Programming Nov 2. 2015 26/32

 Example U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

For goal
ancestor (Q, kay ),
we can use clause

daughter (X , Y ) → ancestor (Y , X )

with unifier
{ Y /Q, X /kay }
to get subgoal
daughter (kay , Q).

Alan Smaill Logic Programming Nov 2. 2015 27/32

 Choice Points U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

If we use only this rule, then what are the choice points in the
search?
Which clause to pick;
there may be several clauses whose heads match a given query.
This is an OR choice: it is enough for any one such choice to
succeed.
The order to tackle the subgoals;
this is an AND choice: all the subgoals must be shown, but
the order may affect if a derivation is found, depending on the
search strategy used.

Alan Smaill Logic Programming Nov 2. 2015 28/32

 Logic Programming U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

The standard form of logic programming (Prolog and friends) is

based on this fragment of first order logic.
The part of the language that corresponds to this reading of
programs as logical statements and computation as inference in
that logic is called pure Prolog — other features are needed to get
a practical programming language out of this.
A Prolog clause
ancestor(X,Y) :- father(X,Z), ancestor(Z,Y)
is simply an alternative notation for

father (X , Z ) ∧ ancestor (Z , Y ) → ancestor (X , Y )

Alan Smaill Logic Programming Nov 2. 2015 29/32

 Inference strategy U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

The strategy adopted in Prolog for search is to search depth-first,

in a top to bottom (for the OR choices) and left to right for the
AND choices.
Top to bottom: pick the clauses in the order in which they
appear in the program.
Left to right: tackle the subgoals in the order in which they
appear in the chosen clause.

Alan Smaill Logic Programming Nov 2. 2015 30/32

 Properties of the Inference System U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

Good News!
The backchain rule gives a complete inference system with respect
to the standard semantics of first-order logic: for given clauses C
and query Q, if C |= Qθ for some θ, then there is a derivation of
Qθ using the backchain rule.
Bad News!
However: the Prolog inference strategy is incomplete: it may fail
to find a derivation, even when a derivation exists. (Examples are
easy to find.)
Bad News!
Also, it is known that there is no decision procedure for the
problem of showing if a query follows or not from a set of definite
clauses. (This is hard to show)

Alan Smaill Logic Programming Nov 2. 2015 31/32

 Summary U
NI VER
S

IT
TH

Y
O F

H
G
E

R
D I U
N B

Predicate Calculus: syntax, semantics

Definite Clause logic
Substitutions and Unification
Inference System of definite clause logic

Alan Smaill Logic Programming Nov 2. 2015 32/32