;;; -*- Mode: Lisp; Syntax: Common-Lisp; -*- File: logic/horn.lisp

;;;; Logical Reasoning in Horn Clause Knowledge Bases

(defstruct horn-kb
  ;; Index all Horn sentences by the predicate on the right-hand side.
  ;; That is, (=> P (Q x)) would be indexed under Q.
  (table (make-hash-table :test #'eq)))

;;;; Top Level Functions: Horn-Tell, Horn-Ask, Horn-Retract

(defun horn-tell (kb sentence)
  "Add a sentence to a Horn knowledge base.  Warn if its not a Horn sentence."
  (for each clause in (conjuncts (->horn sentence)) do
       ;; Each clause should be of form (=> P (Q x))
       ;; Add this to the end of the hash entry for Q
       (nconcf (gethash (op (arg2 clause)) (horn-kb-table kb))
	       (list clause))))

(defun horn-ask (kb query)
  "Use backward chaining to decide if sentence is true."
  (back-chain kb query))

(defun horn-retract (kb sentence)
  "Delete each conjunct of sentence from KB."
  (for each clause in (conjuncts (->horn sentence)) do
       ;; Each clause should be of form (=> P (Q x))
       ;; Delete this from the hash entry for Q
       (deletef clause (gethash (op (arg2 clause)) (horn-kb-table kb))
		:test #'renaming?)))

;;;; Backward Chaining

(defun back-chain (kb query)
  "Find a solution to the query by backward chaining [p 275]."
  (back-chain-list kb (conjuncts (->cnf query)) +no-bindings+))

(defun back-chain-list (kb goals bindings)
  "Solve the conjunction of goals by backward chaining.
  See [p 275], but notice that this implementation is different.
  It returns only the first answer found, and handles composition differently."
  (cond ((eq bindings +fail+) +fail+)
	((null goals) bindings)
	(t (let ((goal (first goals)))
	     (case (op goal)
	       (FALSE +fail+)
	       (TRUE (back-chain-list kb (rest goals) bindings))
	       (AND (back-chain-list kb (append (conjuncts goal) goals)
				     bindings))
	       (OR (some #'(lambda (disjunct)
			     (back-chain-list kb (cons disjunct goals)
					      bindings))
			 (disjuncts goal)))
	       (NOT +fail+) ; Horn clause provers can't handle NOT
	       (t (some
		   #'(lambda (clause)
		       (let ((new-clause (rename-variables clause)))
			 (back-chain-list
			  kb
			  (append (conjuncts (arg1 new-clause)) (rest goals))
			  (unify goal (arg2 new-clause) bindings))))
		   (gethash (op goal) (horn-kb-table kb)))))))))