Declarative Programming
Negation & More on Search
Geraint A. Wiggins
Professor of Computational Creativity
Department of Computer Science
Vrije Universiteit Brussel
Summary of Lectures 1 & 2
I Using the Prolog system
I Programming style
I Prolog clause syntax
I Predicates
I Clauses
I Heads & Bodies
I Variables
I Full-stops (periods)
I Logical operators: , ; -> \+
I Brackets
I Prolog goal syntax
I Prolog proof strategy
I Introduction to Unification
Negation
I So far, everything we have said fits in with the idea of
PROgramming in LOGic
I So far, truth in terms of our intended interpretation has
been exactly the same as provability in the Prolog
database
I However, one aspect of Prolog does not fit well with
logic, even though we need it often
I Negation is the option of reversing the truth or falsehood
of a predicate
Negation (2)
I For example, given the database
p(a).
p(b).
the question
\+ p(a).
yields the answer
false
I Similarly, the question
\+ p(c).
yields the answer
true
Negation (2)
I Negation in Prolog works by
I trying to prove the negated goal;
I if the goal succeeds, fail the current proof;
I if it fails, then proceed to the next goal as though it had
succeeded (NB careful here!)
I We will consider how this is implemented later on
It is called
Negation As Failure (NAF)
Floundering
I However, consider this goal:
X = 5, \+ ( X = 2 ).
I Now consider this goal:
\+ ( X = 2 ), X = 5.
I Logically, these two are the same – both should succeed,
with X = 5
However, they are not the same in (old-fashioned)
Prolog, because the logical semantics (meaning)
diverges from the procedural semantics (the way of
running the program) at this point
Proof Strategy
I Prolog proof strategy works as follows:
To prove a goal true:
I Start at the top of the database;
and scan down it until you find a clause whose head can
unify with the goal.
If there is no such clause, go back to the last clause you
chose and try to find an alternative to it further down
the database
I If that clause has a body,
Take the body, with any values added by unification,
and start again (recurse), with the first goal
I If that clause doesn’t have a body,
proceed to the next unproved goal
I When there are no more unproven goals, stop
Proof Strategy (2)
Given the database and query:
a(1).
a(2).
b(Y) :- a(Y), \+ c(Y).
c(1).
d(1).
d(2).
?- b(X), d(X).
What happens?
I Select leftmost goal: b(X)
I Start at top of database, and scan down for match under
unification
which gives Y = X
Proof Strategy (3)
a(1).
a(2).
b(Y) :- a(Y), \+ c(Y).
c(1).
d(1).
d(2).
I Now we have these goals to consider:
a(X), \+ c(X), d(X).
I Looking for a proof of a(X), we first unify with a(1) to
give X = 1:
\+ c(1), d(1).
I But c(1) is provable, so \+ c(1) fails!
Proof Strategy (4)
a(1).
a(2).
b(Y) :- a(Y), \+ c(Y).
c(1).
d(1).
d(2).
I The last match we made was with a(1), so retry that
. . . and this time a(2) matches.
I So now we have to prove
\+ c(2), d(2).
I We cannot prove c(2), so \+ c(2) succeeds.
Proof Strategy (5)
a(1).
a(2).
b(Y) :- a(Y), \+ c(Y).
c(1).
d(1).
d(2).
I We now have to prove d(2) – which succeeds.
I We finish with the answer
X = 2
yes
Summary
I In this lecture, we have covered:
I Negation As Failure
I Prolog standard proof (search) strategy