:  Implementation Notes:
;
; Following is the core part of the inference engine portion of an expert system, if
; that expert system were designed only to deal with first order logic, with no 
; unification, and only handle propositional sentences in CNF form.  This core engine
; is designed to provide Resolution as used to product a Refutation- it doesn't
; do anything else.


; get_parts_reversed
;
; this takes statements in the form ( foo (not bar) barbar (not foofoo) )
; and finds their opposite, and separates them (ala DeMorgan's Law) into:
;
;  (not foo)  (bar)  (not barbar)  (foofoo)
;
;  which are implicitly anded together into *results*, a global variable
;

(defun get_parts_reversed (mylist)
;(print "in get_parts_reversed")
	(setq lastnot 'not)
	(dolist (x mylist)
		(cond 
			( (equal x 'not) (setq lastnot nil) )
			( (listp x ) (get_parts_reversed x) )
			(t 
				(if (equal lastnot 'not) 
					(setq *results* (cons (list 'not x) *results*))
					(setq *results* (cons (list x) *results*))
				)
			)
		)
	)
)

; flatten
;
; this is helpful if you want to do a simple comparison using member
;
(defun flatten (lst)
	(cond 
		((null lst) nil)
		((atom lst) (list lst) )
		(t (append (flatten (car lst))(flatten (cdr lst)) ))
	)
)

; in_state_space
;
; i use this to do a quick check to see whether someone is passing in something
; that is not in the state space (and therefore, not resolveable)
;

(defun in_state_space(myclause myrules)
  (let ((retval 't))
	(setq a (flatten myclause))
	(setq b (flatten myrules))
	(dolist (x a)
		(when (not (equal x 'not))
			(when (null (member x b) )  (setq retval nil))
		)
	)
  retval)
)

; resolve 
;
; this function attempts to resolve a "statement" against a knowledge base using resolution 
; refutation.  It adds the negation of myclause to the rules in the knowledge base to create
; an in memory (runtime) knowledge base (variable is called: openlist).   This runtime kb is
; then expanded into a list of pairs which is the initial state space  (this variable is 
; called: workingmemory).  The refutation engine then maps (not x) to (x) and reduces the
; statement pairs until (nil nil) is reached.
;
; During resolution a new pairing can be "generated".  The fact is checked against the openlist,
; and if it really is new, it is added to the openlist.  The "new fact" in turn generates new possible
; facts by being recombined with the openlist.  This process is the same as expanding the state space
; of the search by opening a node, and the new facts are in workingmemory.
;
; If a pair of facts ever resolve to an empty clause (contradiction), then the program halts,
; and returns the working knowledgebase (openlist).  The program returns nil if myclause could 
; not be solved.

(defun resolve (myclause myrules)

	(when (not (in_state_space myclause myrules) ) (print "item not in state space") (print "done!") (bye))

; reverse the 'polarity' of input for resolution refutation and separate into CNF (by DeMorgan's Law)
; takes:   ( (not foo) bar etc..)
; applies: (NOT ( (not foo) bar etc...) )
; returns: (foo)  AND  (not bar)  AND  (etc..)
	(get_parts_reversed myclause) 

; *results* contains new list which is added to open list, along with all of the knowledgebase rules
	(setq openlist (cons *results* myrules))

; this generates all possible pairs to compare from openlist- it maps everything onto everything
	(setq workingmemory 
		(do
			((curr openlist (cdr curr)) (apair nil)) ((null (cdr curr)) apair)
			(setq apair (append apair (mapcar #'(lambda (x) (list (car curr) x)) (cdr curr))))
		)
	)
; this does the 'resolution' bit by performing resolution on pairs
	(do ((success nil))
		((or (null workingmemory) success) (nreverse success))

; get next pair
		(setq pair (car workingmemory)) 

; remove that pair from working memory
		(setq workingmemory (cdr workingmemory)) 

;(if (null workingmemory) (print "alert-null working memory"))

; do resolution on that pair - one could have resolved to nil already
		(setq solution (resolve_clauses (car pair) (cadr pair))) 

; if solution exists, recombine the solution we found with existing knowledge to create new inferences
; this could be optimized by checking the solution against the open list first

		(when (and (not (equal solution 'f))  (equal (find_match solution *myglobal*) nil) )

;(if (find_nil solution) (print "alert solution"))

			(setq *myglobal* (append *myglobal* (list solution)))  

			(setq tempsoln nil)
			(dolist (element solution)
; sometimes the same solution kicks back the same element more than once- this is an optimization
; to handle that problem- keep track of a closed list for solution - it only matters when you have
; a really large knowledge base 
				(when (equal (find_match element tempsoln) nil)
					(if (listp element) (setq temp (car element)) (setq temp element))
					(setq recombinants (mapcar #'(lambda (x) (list x element)) openlist))
					(setq workingmemory (append workingmemory recombinants))
; (print (list "alert: element" element "recombinants" recombinants))
					(setq tempsoln (append (list element) tempsoln) )
				)
			)

			(setq openlist (append openlist tempsoln) )

;debug
			(print (list "alert- inference:" tempsoln))

			(if (find_nil solution) (setq success openlist))
		)
	)
)

; this only works for (nil nil), which is the format the working list
; should be reduced to when there are no items left-- 
(defun find_nil(solution)
;(print "in find_nil")
  (let ((retval nil))
	(setq p1 (car solution))
	(setq p2 (cdr solution))
	(if (listp p1) (setq p1 (car p1)))
	(if (listp p2) (setq p2 (car p2)))
	(when (and (null p1) (null p2) ) (setq retval 't))
  retval)
)

; if the items on the list on the left equal a list on the right, this algorithm should find it
; this algorithm looks for an exact match
(defun find_match(solution openlist)
;(print "in find_match")
  (let ((retval nil))
	(dolist (a openlist)
		(setq temp (match solution a))
		(when (equal temp 't) (setq retval 't))
	)
;(when (equal retval 't) (print (list "to match:" solution "match in" openlist "result nil/T:" retval)))
  retval)
)

; the brains behind the find_match function
(defun match (p1 p2)
;(print "in match")
  (let ((retval 't))
	(cond 
		((and (null p1) (null p2)) (setq retval 't))
		((and (atom p1) (atom p2) (equal p1 p2)) (setq retval 't))
		((and (atom p1) (listp p2)) (setq retval nil))
		((and (atom p2) (listp p1)) (setq retval nil))
		((and (listp p1) (listp p2)) 
			(dolist (a p1)
				(setq b (car p2))
				(setq p2 (cdr p2))
				(setq c (match a b))
				(when (null c) (setq retval nil))
			)
		)
		(t (setq retval nil))
	)
;(print (list "matching:" p1 p2 "result" retval))
  retval)
)

; this looks for opposites in pairings, first by checking all the not items in List2 against opposite items
; in List2, and then vice versa- Any opposites are removed and the result put in retval.  

(defun resolve_clauses (L1 L2)
;(print "in resolve_clauses")
  (let ((retval 'f))
	(dolist (item L1)
		(setq negation (find_negation item L2) )
		(when (not (equal negation nil) )
			(when (equal retval 'f) (setq retval nil)) ; we have to return 'f because nil is
							; part of the state space, so when we have something
							; to return, we have to reset retval to hold a list
			(setq newitem1 (remove item L1))
			(setq newitem2 (do_negation item L2))
			(when (equal (car newitem1) 'not) (setq newitem1 nil)) ; (not) is the same as nil
							; during negation sometimes a (not) gets left behind
							; this makes sure that doesn't happen

; this double-check for nil is probably not necessary, but guarantess (nil nil) will be returned in the right
; format if for some reason it is not
			(if (and (null newitem1) (null newitem2))
				(setq retval (list nil nil) )
				(setq retval (append (list newitem1 newitem2) retval ) )
			)
;(print (list "result list1:" L2 newitem1 newitem2))
		)
	)
	(dolist (item L2)
		(setq negation (find_negation item L1) )
		(when (not (equal negation nil) ) 
			(when (equal retval 'f) (setq retval nil)) ; we have to return 'f because nil is
							; part of the state space, so when we have something
							; to return, we have to reset retval to hold a list
			(setq newitem1 (remove item L2))
			(setq newitem2 (do_negation item L1))
			(when (equal (car newitem1) 'not) (setq newitem1 nil)) ; (not) is the same as nil
							; during negation sometimes a (not) gets left behind
							; this makes sure that doesn't happen

; this double-check for nil is probably not necessary, but guarantess (nil nil) will be returned in the right
; format if for some reason it is not
			(if (and (null newitem1) (null newitem2))
				(setq retval (list nil nil) )
				(setq retval (append (list newitem1 newitem2) retval ) )
			)
;(print (list "result list2:" L1 newitem1 newitem2))
		)
	)
  retval)
)

; removes item from mylist, no matter how ugly mylist (or item) is

(defun do_negation(item mylist)
;(print "in do_negation")
  (setq itemnot nil)
  (setq listnot nil)

; handle issues relating to input- we could get (not item) or (item) or item or not item
  (if (listp item) 
	(if (equal (car item) 'not)
		(and (setq itemnot 'not) (setq nolist (cdr item)))
		(setq nolist (car item))
	)
	(setq nolist item)
  )

; do the negation
  (let ((retval nil))
	(dolist (x mylist)
		(cond 
			( (and (atom x) (equal x 'not)) (setq listnot 'not) )
			( (listp x ) (setq retval (append retval (do_negation item x) ) ) )
			( (and (equal listnot 'not) (equal itemnot nil) (equal nolist x))
;				(print (list "alert- doing negation1:" x listnot itemnot)) 
				(setq listnot nil)
			)
			( (and (equal listnot nil) (equal itemnot 'not) (equal (car nolist) x))
;				(print (list "alert- doing negation2:" x listnot itemnot)) 
				(setq listnot nil)
			)
			( (and (not (null x)) (equal listnot 'not) (not (equal nolist x) ) )
				(setq retval (append (list (cons 'not (list x))) retval ) )
				(setq listnot nil)
			)
			(t (setq retval (append retval (list (list x) ) ) ) )
		)
	)
  retval)
)

; finds item to negate in mylist, no matter how ugly mylist (or item) is

(defun find_negation(item mylist)
;(print "in find_negation")
  (setq itemnot nil)
  (setq listnot nil)
  (setq temp nil)

; handle issues relating to input- we could get (not item) or (item) or item or not item
  (if (listp item) 
	(if (equal (car item) 'not)
		(and (setq itemnot 'not) (setq nolist (cdr item)))
		( setq nolist (car item))
	)
	(setq nolist item)
  )

; find the negation, if any - different logic than removing negation
  (let ((retval nil))
	(dolist (x mylist)
		(cond 
			( (and (atom x) (equal x 'not)) (setq listnot 'not) )
			( (listp x ) (setq temp (find_negation item x)) )
			(t 
				(when (and (equal listnot 'not) (equal itemnot nil) (equal nolist x) )
					(setq retval (append retval (list x)) )
;					(print (list "alert- found negation1:" x listnot itemnot)) 
				)
				(when (and (equal listnot nil) (equal itemnot 'not) (equal (car nolist) x) )
					(setq retval (append retval (list x)) )
;					(print (list "alert- found negation2:" x listnot itemnot)) 
				)
				(setq listnot nil)
			)
		)
		(if (not (null temp) ) (setq retval temp))
	)
  retval)
)

(defun doresolve (input mykb)
	(setq *results* '())
	(setq *myglobal* '())
	(resolve input mykb)
)


;; ------------------------------------
; TEST CASE supremo- this one is hard
; this one works in mysterious ways
;; ------------------------------------
;(setq mykb '(
;( red fire (not b) c f (not lisp) pain (not white) )
;( yellow a g final white (not blue) )
;( blue (not happy) sad )
;( emerald thunder black )
;( f (not g) yellow fire )
;( f (not fire) smoke yelow )
;( (not emerald) rain (not thunder) )
;( red sad g lisp white )
;( blue pain (not smoke) )
;( pain c (not diamond) )
;( rain shine )
;( white black )
;( d diamond (not green) )
;( fire happy (not purple) )
;( (not c) (not lisp) )
;( a final e (not white) )
;( blue (not fire) )
;( ruby (not purple) )
;( pain c lisp f )
;( happy e b (not fever) )
;( red (not yellow) )
;( (not final) )
;( c sad white (not green) )
;( ruby (not orange) fever )
;( blue (not black) )
;( (not pain) (not fire) thunder (not a) (not happy) )
;( (not yellow) purple )
;( red d (not green) white black )
;( (not sad) e )
;( (not blue) emerald )
;( fire (not final) fever )
;( (not a) lisp (not c) (not d) (not f) )
;( (not smoke) (not red) (not ruby) )
;( (not fire) (not fever) (not lisp) )
;( ruby rain (not pain) (not g) )
;( smoke (not happy) e )
;( (not fire) (not white) )
;( (not red) final (not f) (black) )
;( (not ruby) fever c thunder (not lightning) )
;( emerald green (not shine) (not d) )
;(NIL (SHINE))  ; for testing find
;))
;(setq myclause '(NIL (SHINE)) ) ; for testing find function - IGNORE 
;(setq myclause '( (tofurkey) )) ; doesn't resolve
;(setq myclause '( not emerald ) )  ; RESOLVES by attrition
;(setq myclause '( emerald ) ) ; RESOLVES by attrition
;
; doesn't complete in a tractable amount of time
;(setq myclause '( sad e) ) ; RESOLVES (amazingly)
;(setq myclause '( (not sad) (not e)) ) ; RESOLVES (amazingly)
;(setq myclause '( emerald green (not shine) (not d) ) )
;(setq myclause '( (not emerald) (not shine) (not diamond) (not fire)))
;(setq myclause '( a b c d e f g ) )
;(setq myclause '( (not fire)(not white) )) ; doesn't resolve
;(setq myclause '( (not lightning)))

;; ------------------------------------
; ANOTHER test CASE - this one is  not a good example
;(setq mykb '(
; ((not parent) ed george )
; ((not parent) linda (not judy) )
; ((parent fred adam judy) )
; ((daugther linda ) )
; ((son ed) )
;))
;(setq myclause '(parent linda (not fred))) ; No resolve
;(setq myclause '( (not parent) fred)) ;  NO resolve
;(setq myclause '(parent (not fred))) ;  NO resolve
;(setq myclause '((not fred))) ; NO resolve
;(setq myclause '((fred))) ;  NO resolve
;(setq myclause '( son ed )) ;  DOES RESOLVE
;(setq myclause '((not son) ed )) ;  NO resolve
;(setq myclause '( (not fred) (not adam))) ;  NO resolve
;(setq myclause '( (not parent) (not adam))) ; NO resolve

;; ------------------------------------
; ANOTHER test CASE - this one is easier
(setq mykb '(
    (dog)
    (cat)
    ( (cat) (not chihuahua) (dog))
    ( (dog schnauzer))
    ((not cat) (dog))
    ((not mouse) (cat))
    ((not bird) (cat))
    ((not bunny) (dog))
    ((not raccoon) (dog))
    ((not fish) (cat))
))
;(setq myclause '( cat (not fish)))  ; RESOLVES
;(setq myclause '(  dog (not raccoon)))  ; RESOLVES
;(setq myclause '( (dog))) ; RESOLVES!
;(setq myclause '( (not dog))) ; nope
(setq myclause '( dog chihuahua)) ; RESOLVES!
;(setq myclause '( (not cat))) ; RESOLVES!
;(setq myclause '( cat)) ; RESOLVES!
;(setq myclause '( gopher)) ; nope
;(setq myclause '( cat (not gopher)))  ; nope
;(setq myclause '( cat gopher))  ; nope
;(setq myclause '( dog cat)) ; RESOLVES!

;; ------------------------------------
; ANOTHER test CASE - this is easy
;(setq mykb '(
;    (bat_ok)
;    ((not moves))
;    ((not bat_ok) (not liftable) moves)
;))
;(setq myclause '( bat_ok)) ; RESOLVES!
;(setq myclause '( not liftable)) ; RESOLVES!
;(setq myclause '( liftable)) ; doesn't resolve
;(setq myclause '( tofurkey)) ; doesn't resolve

(doresolve myclause mykb)



; FUNCTION TESTING --- IGNORE

; test find match - works great!
;(find_match myclause mykb)

;(setq myclause '( NOT RED ))
;(setq myclause '( RED ))
;(setq myclause '( BLACK ))
;(setq myclause '( NOT BLACK ))
;(setq mykb '((NOT BLACK) (NOT WHITE) RED D))
;(setq mykb '((BLACK) (WHITE) (NOT RED) D))
;(find_negation myclause mykb)
;(do_negation myclause mykb)