CS 244/444 Prolog - 26 Oct 2010

Horn clause
	all negative: [~p, ~q]
	or one positive: [p, ~q] == q=>p
	Horn with a positive literal = definite clause
	
	Intuition: 
	definite clause = rule
		A X . birthplace(X,us) => citizen(X)
		[~birthplace(X,us), citizen(X,us)]
	positive unary clause = fact
		birthplace(sam,us)
	negative unary clause = negated goal 
		~citizen(sam,us)
	negative Horn clause = a "no good"
		[~citizen(X,us) v ~citizen(X,russia)]
	not allowed:
		citizen(X,us) v citizen(X,russia)
		citizen(sam,us) v citizen(sam,russia)


SLD resolution = selected literal definite clause resolution
	A sequence of clauses c1, c2, ..., cn
	where
	c1 in S
	ci+1 is the resolvant of ci and some clause in S

	      *	c1
	       \|
	      *	c2
	       \|
		c3

	Observations:
	If cn is  positive, then all the ci are positive.	
	If cn is [], then all the ci are negative.

	Example SLD resolution derivation (not a refutation!)
	Given:
		[~birthplace(X,us), citizen(X,us)]
		[~citizen(X,us), ~over18(X), votes(X,us)]
		[birthplace(sam,us)]
		[over18(sam)]

		[birthplace(sam,us)]
		|		
		[citizen(sam,us)]
		|
		[~over18(X), votes(X,us)]
		|
		[votes(sam,US)]


	Theorem: There is a derivation of a negative
	clause (including []) from a set of Horn
	clauses S iff there is an SLD resolution derivation.

	SLD refutation of a query P (a single positive literal)
	= an SLD resolution derivation of [] where c1 = [~P]

	Example SLD resolution refutation proof:
	Given:
		[~birthplace(X,us), citizen(X,us)]
		[~citizen(X,us), ~over18(X), votes(X,us)]
		[birthplace(sam,us)]
		[over18(sam)]

		Prove: votes(sam,us)

		[~votes(sam,us)]
		|
		[~citizen(sam,us),~over18(sam)]
		|
		[~birthplace(sam,us),~over18(sam)]
		|
		[~over18(sam)]
		|
		[]

Backward chaining: recursively construct an SLD refutation 
proof starting with a set of one or more queries (goals).

Solve [q1,q2,...,qn]
   if n == 0 then return YES
   for each clause [q',~p1,~p2,...,~pm] in KB do
	if unify(q1, q', THETA) and
	   Solve(p1 THETA, p2 THETA, ..., pm THETA, q2, ... qn)
	then return YES
   end for
   return NO

Note that the goals are *implicitly* negated.

This algorithm is:
- backward chaining - from goals to facts
- depth-first - tries new goals pi before old goals q2, ...
- left to right: solves goals in order p1, p2, ...
- top to bottom: tries to find unifiable and solvable clause
	in KB in order from first to last clause

Can be inefficient if same goals appear repeatedly.  Example:

graduate & thesis => honors
senior & requirements => graduate
paper & requirements => thesis
okGPA & okhours & tuitionpaid => requirements

senior
paper
okGPA
okhours
tuitionpaid

Prove: honors
	Solve [honors]
	Solve [graduate, thesis]
	Solve [senior, requirements, thesis]
	Solve [requirements, thesis]
	Solve [okGPA, okhours, tuitionpaid, thesis]
	Solve [okhours, tuitionpaid, thesis]
	Solve [tuitionpaid, thesis]
	Solve [thesis]
	Solve [paper, requirements]
	Solve [requirements]
***>	Solve [okGPA, okhours, tuitionpaid]
	Solve [okhours, tuitionpaid]
	Solve [tuitionpaid]
	Solve []


The corresponding SLD resolution:
	 [~honors]
	 [~graduate, ~thesis]
	 [~senior, ~requirements, ~thesis]
	 [~requirements, ~thesis]
	 [~okGPA, ~okhours, ~tuitionpaid, ~thesis]
	 [~okhours, ~tuitionpaid, ~thesis]
	 [~tuitionpaid, ~thesis]
	 [~thesis]
	 [~paper, ~requirements]
	 [~requirements]
***>	 [~okGPA, ~okhours, ~tuitionpaid]
	 [~okhours, ~tuitionpaid]
	 [~tuitionpaid]
	 []



Is there a way to reduce this redundacy?  To do so, we'd need to
remember that we already solved "requirements", and at ***>
immediately replace "requirements" by [].  Note that this 
corresponds to proofs that are non-linear (not SLD).

In the propositional case, we can use forward chaining to 
achieve the same effect.  The idea is to start with the unit *positive*
clauses in the KB, and use SLD resolution to repeatedly infer
positive clauses.  Add derived positive clauses back to the KB.

	**> Theorem: There is a derivation of a positive unit
	from a set of Horn clauses S iff there is an SLD 
	resolution derivation.

graduate & thesis => honors
senior & requirements => graduate
paper & requirements => thesis
okGPA & okhours & tuitionpaid => requirements

senior
paper
okGPA
okhours
tuitionpaid

	[okGPA]
	[~okhours,~tuitionpaid,requirements]
	[~tuitionpaid,requirements]
	[requirements]
	
Now, add requirements to KB

	[senior]
	[~requirements,graduate]
	[graduate]

Now, add graduate to KB

	[paper]
	[~requirements,thesis]
	[thesis]

Now, add thesis to KB
	[graduate]
	[~thesis, honors]
	[honors]

Add honors to KB.