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

;;;; Testing Logical Inference

(deftest logic
  "Some simple examples in Propositional Logic"
  "First, just test the infix reader."
  ((logic "P=>Q <=> ~Q=>~P") '(<=> (=> P Q) (=> (not Q) (not P))))
  "Print a truth table, as on [p 169]."
  ((truth-table "(P | H) ^ ~H => P"))

  "Some simple examples"
  ((validity "P=>Q <=> ~Q=>~P") 'valid)
  ((validity "SillyQuestion") 'satisfiable)
  ((validity "~SillyQuestion") 'satisfiable)
  ((validity "ToBe or not ToBe") 'valid)
  ((validity "ToBe and not Tobe") 'unsatisfiable)
  ((validity "((S => W1|W2|W3|W4) ^ S ^ (~W1^~W2^~W3)) => W4") 'valid)
  ((validity "Ok ^ (Ok <=> ~W^~P) => ~W") 'valid)
  ((setf kb (make-prop-kb)))
  ((tell kb "S => W1|W2|W3|W4"))
  ((tell kb "S"))
  ((tell kb "~W1"))
  ((tell kb "~W2"))
  ((ask kb "W4") 'nil)
  ((tell kb "~W3"))
  ((ask kb "W4") 't)
  ((tell kb "Ok <=> ~W ^ ~P"))
  ((tell kb "Ok"))
  ((ask kb "W") 'nil)
  ((ask kb "~W") 't)
  ((tell kb "ToBe ^ ~ToBe"))
  ((ask kb "SillyQuestion") 't)

  "Use the KB to solve the `Wumpus at [1,3]' problem [p 174-176]."
  "(This builds a KB with 12 propositional symbols -- about the max.)"
  ((setq kb (make-prop-kb)))
  "The initial state of knowledge"
  ((tell kb "~S11 ^ ~S21 ^S12 ^ ~B11 ^ B21 ^ ~B12"))
  "Rules R1 through R4"
  ((tell kb "~S11 => ~W11 ^ ~W12 ^ ~W21"))
  ((tell kb "~S21 => ~W11 ^ ~W21 ^ ~W22 ^ ~W31"))
  ((tell kb "~S12 => ~W11 ^ ~W12 ^ ~W22 ^ ~W13"))
  ((tell kb "S12 => W13 | W12 | W22 | W11"))
  "Now the query"
  ((ask kb "W13") 't)

  "Now a quick demo of the Horn Logic backward chainer."
  ((setf kb2 (make-horn-kb)))
  ((tell kb2 '(all (x y) (member x (cons x y)))))
  ((tell kb2 '(all (x) (= x x))))
  ((tell kb2 '(=> (member ?x ?rest) (member ?x (cons ?y ?rest)))))
  ((ask-pattern kb2 '?x '(and (member ?x (cons 1 (cons 2 (cons 3))))
			      (= ?x 2))) '2)
  "Now the 'Criminal' problem from [p 271-272]."
  ((setf kb2 (make-horn-kb)))
  ((tell kb2 "American(x) ^ Weapon(y) ^ Nation(z) ^ Hostile(z) ^ Sells(x,z,y)
		 => Criminal(x)"))
  ((tell kb2 "Owns(Nono,M1)"))
  ((tell kb2 "Missle(M1)"))
  ((tell kb2 "Owns(Nono,x) ^ Missle(x) => Sells(West,Nono,x)"))
  ((tell kb2 "Missle(x) => Weapon(x)"))
  ((tell kb2 "Enemy(x,America) => Hostile(x)"))
  ((tell kb2 "American(West)"))
  ((tell kb2 "Nation(Nono)"))
  ((tell kb2 "Enemy(Nono,America)"))
  ((tell kb2 "Nation(America)"))
  ((ask kb2 "Criminal(West)") *)
  ((ask-pattern kb2 "x" "Criminal(x)") 'West)

  )