;;; ================================================================
;;; Conversion to CNF
;;; ================================================================

;;; with syntactic bugs

 [These examples should all trigger errors.]

(FOPC->CNF '(or (forall ?x (exists ?y (inside ?x ?y)))))
(FOPC->CNF '(or (forall ?x (exists ?y (inside ?x ?y))) (> (f ?z) M)))
(FOPC->CNF '(implies (forall ?x (exists ?y (inside ?x ?y)))))
(FOPC->CNF '(iff (forall ?x (inside ?x foo)) (> (f ?x) M)))


;;; check expansion of iff and implies

(FOPC->CNF '(iff (forall ?x (exists ?y (inside ?x ?y))) (forall ?z (> (f ?z) M))))
--> '(#{Sentence ((inside ?X-15 (Y-13 ?X-15)) (not (> (f Z-14) m)))} 
      #{Sentence ((> (f ?Z-17) m) (not (inside X-12 ?Y-16)))})

(FOPC->CNF '(implies (forall ?x (exists ?y (inside ?x ?y))) (forall ?z (> (f ?z) M))))
--> '(#{Sentence ((> (f ?Z-11) m) (not (inside X-7 ?Y-10)))})

;;; checking that not moves inwards properly 

(FOPC->CNF '(not (forall ?x (exists ?y (inside ?x ?y)))))
--> '(#{Sentence ((not (inside X-18 ?Y-20)))})

(FOPC->CNF '(not (exists ?x (forall ?y (inside ?x ?y)))))
--> '(#{Sentence ((not (inside ?X-23 (Y-22 ?X-23))))})

(FOPC->CNF '(not (and (forall ?room (empty ?room)) (> pi 23))))
--> '(#{Sentence ((not (empty ROOM-24)) (not (> pi 23)))})

(FOPC->CNF '(not (or (forall ?room (empty ?room)) (> pi 23))))
--> '(#{Sentence ((not (empty ROOM-25)))} #{Sentence ((not (> pi 23)))})

(FOPC->CNF '(not (or (not (forall ?room (empty ?room))) (> pi 23))))
--> '(#{Sentence ((empty ?ROOM-27))} #{Sentence ((not (> pi 23)))})

(FOPC->CNF 
  '(not (exists ?z (or (and (funny ?z) (not (forall ?room (empty ?room)))) (> pi 23)))))
--> '(#{Sentence ((not (funny ?Z-31)) (empty ?ROOM-30))} #{Sentence ((not (> pi 23)))})


;;; handling quantifiers e.g. variable renaming, elimnating existential
;;;     quantifiers using Skolem variables (see also the examples for
;;;     checking the not-movement step)

(FOPC->CNF '(forall ?x (exists ?y (inside ?x ?y))))
--> '(#{Sentence ((inside ?X-34 (Y-33 ?X-34)))})

(FOPC->CNF '(or (forall ?x (exists ?y (inside ?x ?y))) (forall ?z (> (f ?z) M))))
--> '(#{Sentence ((inside ?X-39 (Y-36 ?X-39)) (> (f ?Z-38) m))})

(FOPC->CNF '(forall ?x (iff (> M ?x) (up (f ?x) q))))
--> '(#{Sentence ((> m ?X-41) (not (up (f ?X-41) q)))} 
      #{Sentence ((up (f ?X-42) q) (not (> m ?X-42)))})

(FOPC->CNF '(forall ?x (and (exists ?m (foo ?m))
                     (forall ?z (exists ?y (and (inside ?x ?y) (> (f ?z) M)))))))
--> '(#{Sentence ((foo (M-44 ?X-47)))} #{Sentence ((inside ?X-48 (Y-46 ?Z-49 ?X-48)))} 
      #{Sentence ((> (f ?Z-50) m))})

(FOPC->CNF '(not (exists ?z (or (and (funny ?z) (not (forall ?room (empty ?room)))) (> pi 23)))))
--> '(#{Sentence ((not (funny ?Z-54)) (empty ?ROOM-53))} #{Sentence ((not (> pi 23)))})

;;; distributive law

(FOPC->CNF '(or (and (f a) (g b)) (p c)))
--> '(#{Sentence ((f a) (p c))} #{Sentence ((g b) (p c))})

(FOPC->CNF '(or (and (f a) (g b)) (and (M x) (p c))))
--> '(#{Sentence ((f a) (m x))} #{Sentence ((f a) (p c))} 
      #{Sentence ((g b) (m x))} #{Sentence ((g b) (p c))})

;;; ================================================================
;;; Examples for testing the search engine
;;; ================================================================

;;; *small-food-facts* is sufficient to prove the goal '(in beans bottom-shelf)

;;; *food-facts is sufficient to prove the goals
;;;    '(goes-in chickpeas bottom-shelf))
;;;    '(same-shelf clove saffron))
;;;    '(same-shelf tomatoes beans))
;;;    '(not (out tomatoes))
;;;    '(same-shelf beans tomatoes)
;;;    '(same-shelf tomatoes beans) 
;;;    '(goes-in chickpeas bottom-shelf) 
;;;    '(goes-in tomatoes bottom-shelf) 
;;; Some of these, however, only finish in a reasonable number of iterations
;;;    if you use a good search strategy.


(define *small-food-facts*
  '(
    (forall ?x 
	    (forall ?y 
		    (implies
		     (and (goes-in ?x ?y) (not (out ?x)))
		     (in ?x ?y))))
    (forall ?x (implies (and (canned ?x) (vegetable ?x))
			(goes-in ?x bottom-shelf)))
    (canned beans)
    (vegetable beans)
    (not (out beans))))

(define *additional-food-facts*
  '(
    (forall ?x 
	    (forall ?y 
		    (forall ?z
			    (implies (and (same-shelf ?x ?y) (goes-in ?x ?z))
				     (goes-in ?y ?z)))))
    (forall ?x (forall ?y (implies (same-shelf ?x ?y) (same-shelf ?y ?x))))
    (forall ?x (forall ?y (forall ?z
         (implies (and (same-shelf ?x ?y) (same-shelf ?y ?z))
                       (same-shelf ?x ?z)))))
    (forall ?x (same-shelf ?x ?x))
    (not (out chickpeas))
    (same-shelf chickpeas beans)
    (forall ?x (forall ?y (implies (and (spice ?x) (spice ?y)) (same-shelf ?x ?y))))
    (spice clove)
    (spice saffron)
    (forall ?x (iff (not (put-away ?x)) (out ?x)))
    (put-away tomatoes)
    (same-shelf tomatoes chickpeas)))

(define *food-facts*
  (append *small-food-facts* *additional-food-facts*))