Horn clauses
Clauses are used two ways:
• asdisjunctions:! (rain∨sleet)
• asimplications:! (¬child∨¬male∨boy)
Here focus on 2nd use
Horn clause = at most one +ve literal in clause • positive / definite clause = exactly one +ve literal
! [¬p1, ¬p2, …, ¬pn, q]
• negative clause = no +ve literals
! [¬p1, ¬p2, …, ¬pn] Note
! [¬p1, ¬p2, …, ¬pn, q] is a representation for
! (¬p1 ∨¬p2 ∨ … ∨¬pn ∨q)!or
! [(p1∧p2∧…∧pn) ⊃q]
So can read as
! If p1 and p2 and …and pn thenq
and write sometimes as
! ! p1∧p2∧…∧pn ⇒q
KR & R! © Brachman & Levesque 2005 Horn Logic
Resolution with Horn clauses
Only two possibilities:
Neg Pos Pos Pos
Neg Pos
It is possible to rearrange derivations (of negative clauses) so that all new derived clauses are negative clauses
[γ, ¬p] [α, ¬q, p]
[α, ¬q, p] [β, q] [ p, α,β]
[α,γ,¬q]
[α, β, γ]
[β,q]
the α, β, γare
negative lits
[γ,¬p]
[α, β, γ]
derived positive clause to eliminate
Can also change derivations such that each derived clause is a resolvent of the previous derived one (-ve) and some +ve clause in the original set of clauses
! Since each derived clause is negative, one parent must be positive (and so from original set) and one negative.
! Continue working backwards until both parents of derived clause are from the original set of clauses
! Eliminate all other clauses not on direct path
KR & R! © Brachman & Levesque 2005 Horn Logic
SLD Resolution
Recurring pattern in derivations:
See previously: • example1
• example3
c1
old
new
cn
An SLD-derivation of a clause c from a set of clauses S is a sequence of clause c1, c2, … cn
such that cn = c, and
c2 • arithmeticexample c3
But not:
• example2 cn-1 • 3blockexample
c1 ∈S
ci+1 is a resolvent of ci and a clause
Note: SLD derivation is just a special form of
derivation and where we leave out the elements of S
D(efinite) clauses
1.!
2.!
in S
SLD
Write: S |⎯ c SLD means S(elected) literals L(inear) form
(except c ) 1
KR & R! © Brachman & Levesque 2005 Horn Logic
Completeness of SLD
In general, cannot restrict Resolution steps to always use a clause that is in the original set
Proof:
! S = {[p, q], [p, ¬q], [¬p, q] [¬p, ¬q]}
* * * then S|⎯[].
* Need to resolve some [l] and [¬l] to get [].
* But S does not contain any unit clauses.
! So will need to derive both [l] and
[¬l]* * andthenresolvethemtogether. But can do so for Horn clauses…
Theorem: for Horn clauses, H |⎯ [] iff H |⎯ [] SLD
! So: H is unsatisfiable iff H |⎯ [] SLD
! This will considerably simplify the search for derivations
Note: in Horn version of SLD-Resolution, each clause c1, c2, …, cn, will be negative
! So clauses H must always contain at least one negative clause, c1.
KR & R! © Brachman & Levesque 2005 Horn Logic
Example 1 (again)
KB:
! FirstGrade
! FirstGrade ⇒ Child
! Child ∧ Male ⇒ Boy
! Kindergarten ⇒ Child
* Child ∧ Female ⇒ Girl
* Female
Show KB∪{~Girl} unsatisfiable
[¬Girl] goal
[¬Child, ¬Female] [¬Child] [¬FirstGrade]
[]
Girl
or
A goal tree whose nodes are atoms, whose root is the atom to prove, and whose leaves are in the KB
Child Female
solved
FirstGrade
solved
KR & R! © Brachman & Levesque 2005 Horn Logic
Prolog
Horn clauses form the basis of Prolog
Append(nil,y,y)
Append(x,y,z) ⇒ Append(cons(w,x),y,cons(w,z))
Append(cons(a,cons(b,nil)), cons(c,nil), u) u / cons(a,u′)
Append(cons(b,nil), cons(c,nil), u′) u′ / cons(b,u′′)
Append(nil, cons(c,nil), u′′)
solved: u′′ / cons(c,nil)
goal
So goal succeeds with u = cons(a,cons(b,cons(c,nil))) that is: Append([a b],[c],[a b c])
With SLD derivation, can always extract answer from proof ! H |= ∃xα(x) iff forsometermt, H |= α(t)
Different answers can be found by finding other derivations
KR & R! © Brachman & Levesque 2005 Horn Logic
Back-chaining procedure
Satisfiability of a set of Horn clauses with exactly one negative clause
Solve[q1, q2, …, qn] =! /* to establish conjunction of qi */
! If n=0 then return YES; ! /* empty clause detected */
! Foreachd ∈KB do
! If d = [q1, ¬p1, ¬p2, …, ¬pm]* ! ! and ! !
! Solve[p1, p2, …, pm, q2, …, qn]!
/* match first q */ /*replaceqby-velits*/
/* recursively */
! then return YES
! end for; ! /* can’t find a clause to eliminate q */
! Return NO
Depth-first, left-right, back-chaining
• depth-firstbecauseattemptpibeforetryingqi
• left-rightbecausetryqiinorder,1,2,3,…
• back-chainingbecausesearchfromgoalqtofactsinKBp
This is the execution strategy of Prolog
! First-order case requires unification etc.
KR & R! © Brachman & Levesque 2005 Horn Logic
Problems with back-chaining
Can go into infinite loop
! tautologous clause: [p , ¬p]
! corresponds to Prolog program with p :- p.
Previous back-chaining algorithm is inefficient ! Example: consider 2n atoms: p1, …, pn, q1, …, qn
! !
! !
! !
and 4n – 4 clauses:
! (pi ⇒ pi+1), (qi ⇒ pi+1), ! ! (pi ⇒ qi+1), (qi ⇒ qi+1).
with goal pn
has execution tree like this
pn-1
qn-1
pn
pn-2
…
qn-2
…
pn-2
…
qn-2
…
!!
search eventually fails after 2n steps!
KR & R! © Brachman & Levesque 2005 Horn Logic
Forward-chaining
Simple procedure to determine if Horn KB |= q. ! main idea: mark atoms as solved
FirstGrade example:
! Marks: FirstGrade, Child, Female, Girl
! ! then done!
Observe:
• onlylettersinKBcanbemarked,soatmostalinear number of iterations
• not goal-directed, so not always desirable
A similar procedure with better data structures will run in linear time overall
1.!If q is marked as solved, then return YES
2.!Is there a {p1,¬p2, …,¬pn} ∈ KB such that p2, …, pn are marked as solved, but the positive lit p1 is not marked as solved?
! no:! return NO
! yes:! mark p1 as solved, and go to 1.
KR & R! © Brachman & Levesque 2005 Horn Logic
First-order undecidability
Even with just Horn clauses, in the first-order case we still have the possibility of generating an infinite branch of resolvents
KB:! LessThan(succ(x),y) ⇒ LessThan(x,y) Q:! LessThan(zero,zero)
[¬LessThan(0,0)] x/0, y/0
[¬LessThan(1,0)] x/1, y/0
[¬LessThan(2,0)] x/2, y/0
…
As with full clauses, the best that can be expected is to give control of the deduction to the user
! to some extent this is what is done in Prolog, but we will see more in “Procedural Control”
As with full Resolution, there is no way to detect when this will happen
So there is no procedure that will test for satisfiability of first-order Horn clauses
the question is undecidable
KR & R! © Brachman & Levesque 2005 Horn Logic