Horn and Definite clauses
→ A Horn clause is a clause that contains at most
literals
one positive literal and zero or more
negative
→ A definite Korn) clause is a clause
containing exactly
literal and
one
positive zero or more
negative literals .
→ A Unit clause or a fact is a definite clause containing
no
negative literals e- as
( → P)
Logic Programming
→ A (propositional) definite clause
program is a set P
Harn clauses
of definite in rule form
{ }
→ •
P
if
=
→ a
→ R
O → S
R S,
→ T
Queries
→ A conjunctive query is a
conjunction of (positive literals
di In Ii Iz In
A ② A . . .
A , ,
- - - .
→ This is the set of literals that we want to prove given a definite
clause
Natural Deduction vs Resolution
→ Natural Deduction proceeds in forwards direction from
a
premises / data)
the to the conclusion / query)
↳ starting with the data we ask :
that follow from the data
"
"
what are the
necessary consequences
→ Resolution proceeds
data
in a backwards direction from the
to the
query
↳ with the conclusion
starting we ask :
"
what are the sufficient conditions that would prove the query "
Resolution Procedure
step 1) Start with query that
you want
to
prove
( preface with a ? to distinguish query from data)
e :S
?T
step 2) Identify the
first occurrence d- rule from the a
logic program
7 that matches the first conjunct of the
e-
query
9
? T R S ,
→ T
step 3) Replace the conjunct of the query matching the head
of the rule with the tail of the rule
• 9
?T R S ,
→ T
2. Rt S /
,
-
step 4) Repeat until all conjuncts of the query have been eliminated
after having been matched by fact ( with a an
empty tail)
OR
At least one tonjunct is left which fails to match the
head of any rule
e. g 1
?T R ,
S → T → p
p
RFP
→ 0
? → R p → R
¥ O → S
? → P R S ,
→ T
?
% → s
P → ce
? Es p
✓
☐ →
empty box means successful Resolution
step 5) In the event that there are more than one rules whose
head matches the first conjunct of the query , we
need to backtrack if the first rule leads to a
may
deadlock
2
e.
g
? T R→ T → p
?R✓d a → R
→ R P → R
i. R - T
p
e
i Eason → colored box means deadlock on unsuccessful resolution
i
'
?R P→ R
'
✓
P
7-
→
→ Both Natural Deduction and Resolution are syntactic
mechanisms for proving logical consequence since they depend .
on
rewriting rules they only care about the syntactic
,
structure of the formulas encountered and everything can be
performed by simple pattern matching .
→ Resolution procedure can be thought of as applying the
following natural deduction rules in reverse
A,B_ ( )
AsAB→B_ ( NP ) ↳ E)
or and Al
An B
Note Not all propositional
proofs can be achieved using
to the
just these two rules This only works due .
restricted nature of our
logic programs comprising only
definite clauses
