CSI2120 Programming Paradigms Jochen Lang
jlang@uottawa.ca
Faculté de génie | Faculty of Engineering
Jochen Lang, EECS jlang@uOttawa.ca
Logic Programming in Prolog
• Predicate calculus – Predicates
– Horn clauses
– Proof by Contradiction: Resolution
• Search Trees
– Backtracking
Jochen Lang, EECS jlang@uOttawa.ca
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.
Jochen Lang, EECS jlang@uOttawa.ca
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
Jochen Lang, EECS jlang@uOttawa.ca
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.
Jochen Lang, EECS jlang@uOttawa.ca
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
Jochen Lang, EECS jlang@uOttawa.ca
Converting to a Horn Formula
• Implication (a implies b) is the same as – Use truth table to confirm
This may be suprising at first! Because a is false, nothing can be “implied”, b can be true or false, the implication cannot be false. In logic if something is not false, it must be true.
a
b
0
0
true
true
0
1
true
true
1
0
false
false
1
1
true
true
• Equivalence (a equivalent to b) is the same as
Jochen Lang, EECS jlang@uOttawa.ca
Resolution
• Rule of inference for theorem proofing in propositional logic.
• Resolution rule
– For a one-literal clause (modus ponens) →, which
reads ( implies and ) entails
• In other words, as implies and we are asserted that is true, must be true
– Can use for multi-literal clauses ∧ →, , which
reads ( implies and and ) entails
• In other words, as implies and we are asserted that and are true, must be true
Jochen Lang, EECS jlang@uOttawa.ca
Prolog Example using Resolution
• Our program for which we want to proof f to be true. We have the rule f :- a,b.
And the true fact a.
And the true fact b.
• Our program expressed in predicate logic
and and
• Turn Horn formula into CNF
(()()
Jochen Lang, EECS jlang@uOttawa.ca
Proof by Contradiction with Repeated Application of Resolution
• Consider
( ) and and
• Proof by contradiction, i.e., assume
( ) and and and
• Simplify by resolution ((
) and and
) and
which is a contradiction
))and and
(( and
Jochen Lang, EECS jlang@uOttawa.ca
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 .
Jochen Lang, EECS jlang@uOttawa.ca
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.
Jochen Lang, EECS jlang@uOttawa.ca
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.
Jochen Lang, EECS jlang@uOttawa.ca
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.
Jochen Lang, EECS jlang@uOttawa.ca
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
Jochen Lang, EECS jlang@uOttawa.ca
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
Jochen Lang, EECS jlang@uOttawa.ca
A Simple Example
voter(Y) Y=X
name(X), citizen(X), adult(X)
name(joe).
name(jane).
citizen(jane).
citizen(joe).
adult(jane).
voter(X):-
name(X),
citizen(X),
adult(X).
?- voter(Y).
X=joe citizen(joe), adult(joe)
adult(joe)
X=jane citizen(jane), adult(jane)
adult(jane)
Jochen Lang, EECS jlang@uOttawa.ca
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).
Jochen Lang, EECS jlang@uOttawa.ca
Another Example: 3 Versions of
French Nobleman
Version A
father(charles,jean).
noble(henri).
noble(louis).
noble(charles).
noble(X):- father(Y,X),
noble(Y).
Version C
father(charles,jean).
noble(X):- father(Y,X),
noble(Y).
noble(henri).
noble(louis).
noble(charles).
Version B
father(charles,jean).
noble(henri).
noble(louis).
noble(charles).
noble(X):- noble(Y),
father(Y,X).
Source: R. Laganière
?- noble(jean).
Jochen Lang, EECS jlang@uOttawa.ca
A Last Example
likes(peter,jane).
likes(paul,jane).
conflict(X,Y) :- likes(X,Z),likes(Y,Z).
?- conflict(X,Y).
• How many solutions?
Jochen Lang, EECS jlang@uOttawa.ca
Summary
• Predicate calculus – Predicates
– Horn clauses
– Proof by Contradiction: Resolution
• Search Trees
– Backtracking
Jochen Lang, EECS jlang@uOttawa.ca