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