Intro-  The Horn Clause.  The horn structure is a logical structure
	made up entirely of implications ( p => q ).  It establishes truth	
	value by backward chaining. It verifies existance by backward chaining 
        and substitution	



				The (Aima) Horn Clause 

		I chose the Horn Clause, which is a logical method, to 
	investigate.  After a number of days of websearch I found a 
	code source in the Aima files of Norvig and Russell at
	Berkeley.

		It took me several more days to start to get a vague
	idea of the method.  I had heard that it involved backward
	chaining and was starting to get an idea of what this meant.

		On or about Oct 7 upon looking carefully through the 
	Aima files and any container file which seemed vaguely relevant
	I discovered a testfile which contained data which was accepted
	by the program.  Since then my analysis has sped up to about
	snails-pace.
 
		I started by copying the horn.lisp file:
	http://www.cs.berkeley.edu/~russell/code/logic/algorithms/horn.lisp 
	into my file.  The file loaded okay, but I couldn't make horn-kb,
	which was necessary to start the process.  I eventually hit on
	loading the Aima file and the logic files (which I used last
	semester in 223) in addition to the Horn file.  Using this
	system is was possible to run the system as follows:

		 Start the run by loading aima.fasl and aima-loading 'logic. 

	 the initial call is to a constructor of sorts,
**********

	The methods associated with horn-kb are:

                 (setf hkb (make-horn-kb))

		(defmethod tell ((kb horn-kb) sentence)

		(defmethod retract ((kb horn-kb) sentence)

		(defmethod ask-each ((kb horn-kb) query fn)


	and the functions

		(defun ask (kb query)

		(defun ask-pattern (kb query &optional (pattern query))

		(defun ask-patterns (kb query &optional (pattern query))

		(defun back-chain-each (kb goals bindings fn)

	
**********
        (setf hkb (make-horn-kb))
                (table (make-hash-table :test #'eq)))

                ##precondition:  no instance of a structure

                ##postcondition:  An instance of a knowledge structure
                which is capable of indexing Horn statements (in a hash table
		data structure) by the predicate on the right-hand side of 
		the clause.

	(tell ((kb horn-kb) sentence)
		(for each clause in (conjuncts (->horn sentence)) do
        	       (setf (gethash (op (arg2 clause)) (horn-kb-table kb))
                       (nconc (gethash (op (arg2 clause)) (horn-kb-table kb))
                       (list clause)))))

		##precondition:  A horn-kb.

		##postcondition:  Checked sentence to make sure sentence
		 is a Horn clause (e.g. (=> P (Q x))), then sentence is 
		added to the hash table for Q.

		
	(defmethod retract ((kb horn-kb) sentence)
	  (for each clause in (conjuncts (->horn sentence))
        	do
		 (deletef clause (gethash (op (arg2 clause)) 
			(horn-kb-table kb)) :test #'renaming?)))

		##precondition:  The hash table horn-kb made up of 
		horn clauses.  A sentence with q left side. 

		##postcondition:  Each clause which is a conjunct of q
		has been deleted from the table.
		

	(defmethod ask-each ((kb horn-kb) query fn)
	    (back-chain-each kb (conjuncts (->cnf query)) +no-bindings+ fn))	

		##precondition:  The hash table horn-kb made up of Horn
		clauses.  Parameter query.

		##postcondition:  The truth value of the query is ascertained
		by back chaining.

********  the functions ask, ask-pattern and ask-patterns all use ASK-EACH
		to determine the truth value of the query.*******

	(defun ask (kb query)
		  (ask-each kb (logic query)
            #'(lambda (s) (declare (ignore s)) (RETURN-FROM ASK t))))

                ##precondition:  The hash table horn-kb made up of Horn
                clauses.  Parameter query.
		
		##postcondition:  The truth value of the query is returned
		as either t or nil.

	(defun ask-pattern (kb query &optional (pattern query))
		  (ask-each kb (logic query)
            #'(lambda (s) (RETURN-FROM ASK-PATTERN
                            (subst-bindings s (logic pattern))))))

                ##precondition:  The hash table horn-kb made up of Horn
                clauses.   Parameter query.

		##postcondition:  The truth value of the sentence is 
		determined.  If true, bindings are substituted into pattern.


	(defun ask-patterns (kb query &optional (pattern query))
		  (let ((pat (logic pattern))
        		(results nil))
                  (ask-each kb (logic query)
              #'(lambda (s) (push (subst-bindings s pat) results)))
                    (nreverse results)))  ;;Reverses the atoms of the 
					  ;; statement since it comes from
        				  ;; backchaining reversed. 

                ##precondition:  The hash table horn-kb made up of Horn
                clauses.  Parameter query.

		##postcondition:  All proofs of query are found, bindings
		are substituted into each proof and a list of all substituted
		patterns is returned.


	(defun back-chain-each (kb goals bindings fn)
		  (cond ((eq bindings +fail+) +fail+)
				;;If bindings have failed back-chain fails!
        		((null goals) (funcall fn bindings))
				;; if no goals left, recursion stops.
        		(t (let ((goal (first goals)))
                       		;;  First of list is made goal to consider. 
		(case (op goal)    ;;  switch on goal.  
               		(FALSE +fail+)  ;; goal is false => fail.
               		(TRUE (back-chain-each kb (rest goals) bindings fn))
				;;  goal is true recurse using rest of goals.
               		(= (back-chain-each kb (rest goals)
                              (unify (arg1 goal) (arg2 goal) bindings)
                                   fn))
				;; when  goal is = recurse with rest of goals 
				;;  after arg1 and arg2 are matched.
				 
               		(AND (back-chain-each kb 
				(append (conjuncts goal) goals) bindings fn))
				;; when goal is AND recurse after adding a 
				;; list all and's to the end of goals.
               
			(OR (for each disjunct in (disjuncts goal) do
                        (back-chain-each kb (cons disjunct goals) bindings fn)))
                                ;; when goal is OR recurse after adding a 
                                ;; list all or's to the end of goals.

               		(NOT +fail+) ;;when goal is NOT fail!  back-chain
				     ;; does not deal with not. 

                (for each clause in (gethash (op goal) (horn-kb-table kb)) do
                     (let ((new-clause (rename-variables clause)))
                       (back-chain-each  kb
                        (append (conjuncts (arg1 new-clause)) (rest goals))
                        (unify goal (arg2 new-clause) bindings)
                        fn)))))))))
			;;  This is the "thinking part" of the Horn clause
			;;for each hashkey which is op goal makes a new
			;; clause after variable substitution then
			;; recurse after adding the and's in arg1
			;; to rest goals and matching goal and arg2
			;; in the new clause.
		
                ##precondition:  The hash table horn-kb made up of Horn
                clauses.  Parameter goals(var statement).

		##postcondition: returns the statement with valid parts of the
		domain substituted for the variables. 

*****************