Programming
Paradigms
CSI2120
Jochen Lang
EECS, University of Ottawa
Canada
Logic Programming in Prolog
• Predicate calculus
– Predicates
– Horn clauses
– Proof by Contradiction: Resolution
• Search Trees
– Backtracking
CSI2120: Programming Paradigms
Prolog Predicates
• A rule is a clause where the body is non-empty while a fact
is a clause with an empty body. Most rules contain
variables.
• Prolog Definition with an anonymous variable, written as
“_”
salary(X) :- employed(Y,X). % Ok but with
% a warning
– Or with an anonymous variable
salary(X) :- employed(_,X).
• Facts and rules are predicates.
CSI2120: Programming Paradigms
Predicate Calculus
• First Order Logic
– predicate symbols: x,y,z (constants and variables)
• and compound terms
– equality: ≡
– negation:
– logic binary connections: ∨,∧, →
– quantifiers ‘for all …’ and ‘there exists … such that’
• universal quantifier ∀
• existential quantifier ∃
CSI2120: Programming Paradigms
Predicates in Prolog
• ← ∧ ∧ ⋯∧
– All terms , , … , in the body of the predicate have to be
true for the head to be true. Or, , , … , being true,
implies b is true.
• ←
– This is a fact because truth is always implied.
• ←
– Without a head, it is goal for which correctness still needs to
be proven. This may be considered a question in logic
programming in Prolog. Proofing correctness requires
deductive reasoning.
CSI2120: Programming Paradigms
Horn Clauses
• We can express first order logic with Horn* clauses and
solve predicate calculus mechanically
• Horn clauses are the foundation of logic programming
• Horn formulas are the only logic formulas in Prolog
– Atomic (i.e., unique) formulas and their negation. They are
also called literals.
– Disjunction of literals to form clauses
– A Horn clause has exactly one non-negated literal
– Conjunctive normal form (CNF) is a conjunction of Horn
clauses
* Alfred Horn, 1918-2001 American Mathematician
CSI2120: Programming Paradigms
Converting to a Horn Formula
• Implication (a implies b) ⟶ is the same as ∨
• Equivalence (a equivalent to b) ≡ is the same as
∧ ∨ ∧
• Example (Prolog): Proof f to be true.
f :- a,b.
a.
b.
• Predicate logic
( ∧ ⟶ ) and and
• Horn formula
( ( ∧ ∨ )≡( ∨ ∨ )
CSI2120: Programming Paradigms
Proof by Resolution
• Consider
( ∨ ∨ ) and and
• Proof by contradiction, i.e., assume
( ∨ ∨ ) and and and
• Simplify by resolution
(( ∧ ∨ ∨ )) and and
∨ ) and and
(( ∧ ∨ ) and
and which is a contradiction
CSI2120: Programming Paradigms
Prolog and Horn Clauses
• Facts and rules are Horn Clauses as in the example.
• In general F :- F1, F2,…, Fn.
– meaning F if F1 and F2 and …and Fn
– F is an atomic formula
– Fi are terms or their negation
• F is the head of the clause
• F1, F2,…, Fn together are the body of the clause
• To prove F in Prolog, it must be true (proven) that F1, F2,…,
and Fn are true .
CSI2120: Programming Paradigms
Horn Clauses
• Horn clauses can express nearly all logic expressions, all
mathematical algorithms.
• It enables one to establish the truth of a hypothesis by
establishing the truth of terms but it does not allow one to
prove the falsehood of a hypothesis. False in logic
programming only means that the goal can not be proven
correct.
CSI2120: Programming Paradigms
Search Trees
• Search trees represent queries
– Root of the tree is the question
– Nodes (or vertices) are decisions and show which goals still
need to be satisfied
– Transitions (along edges) from one node to the next are the
result of an unification between a goal and a fact or the head
of a rule.
– The edges are a step in the proof.
CSI2120: Programming Paradigms
Nodes in Search Tree
– Goals are ordered from left to right following the order in the
rules. Goals are stated in a node.
– Leaf nodes which contain one or several goals are failure
nodes. The first (left-most) goal caused the failure.
– Empty leaf nodes are success nodes. The path from the root
to the leaf node contains the unifications and steps
necessary for the proof. These can be found on the edges.
CSI2120: Programming Paradigms
Solution Strategy of Prolog
• Prolog builds the search tree from the question as a root
node. The tree is built in a depth-first fashion.
• An empty (leaf) node is a proof or a solution
– Search can continue for other solutions by backtracking and
traversing unexplored branches
• An non-empty leaf node is a failure
– A solution may still be found by backtracking and traversing
unexplored branches
CSI2120: Programming Paradigms
Backtracking
• If there are no more new nodes found, there are no more
solutions and Prolog answers no.
• Termination is not guaranteed. It is easy to write rules that
cause an infinite recursion.
• The order in which solutions are produced depends on the
order in predicates, in particular:
– the order of the literals in the body of clause
– the order of the predicates
CSI2120: Programming Paradigms
voter(Y)
A Simple Example
Y=X
name(joe). name(X), citizen(X),
name(jane). adult(X)
citizen(jane). X=joe
citizen(joe). X=jane
citizen(joe), adult(joe)
adult(jane).
voter(X):- citizen(jane), adult(jane)
name(X),
citizen(X),
adult(joe) adult(jane)
adult(X).
?- voter(Y).
CSI2120: Programming Paradigms
Another Example
Building categories:
parent(building,farmbuilding).
parent(farmbuilding,barn).
parent(farmbuilding,silo).
parent(farmbuilding,house).
parent(barn,horsebarn).
parent(barn,cowbarn).
typeof(X,Y):- parent(Z,X),typeof(Z,Y).
typeof(X,Y):- parent(Y,X).
?- typeof(cowbarn,A).
CSI2120: Programming Paradigms
Another Example: 3 Versions of French
Nobleman
Version C
Version A father(charles,jean).
father(charles,jean). noble(X):- father(Y,X),
noble(henri). noble(Y).
noble(louis). noble(henri).
noble(charles). noble(louis).
noble(X):- father(Y,X), noble(charles).
noble(Y).
Version B
father(charles,jean).
noble(henri).
noble(louis).
noble(charles).
?- noble(jean). noble(X):- noble(Y),
father(Y,X).
Source: R. Laganière
CSI2120: Programming Paradigms
A Last Example
likes(peter,jane).
likes(paul,jane).
conflict(X,Y) :- likes(X,Z),likes(Y,Z).
?- conflict(X,Y).
• How many solutions?
CSI2120: Programming Paradigms
Summary
• Predicate calculus
– Predicates
– Horn clauses
– Proof by Contradiction: Resolution
• Search Trees
– Backtracking
CSI2120: Programming Paradigms
