;;; -*- 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 and ~ToBe"))
  ((ask kb "SillyQuestion") 't)
  
  "A look at Normal forms (conjunctive, implicative, and Horn)."
  ((->cnf '(<=> P Q))
   '(AND (OR P (NOT Q)) (OR (NOT P) Q)))
  ((->inf '(<=> P Q))
   '(AND (=> Q P) (=> P Q)))
  ((->horn '(<=> P Q))
   '(AND (=> Q P) (=> P Q)))
  ((->cnf '(=> (not P) R))
   '(OR R P))
  ((->inf '(=> (not P) R))
   '(=> TRUE (OR R P)))
  
  "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."
  "you can do without starting to slow down."
  ((setq kb1 (make-prop-kb)))
  "The initial state of knowledge"
  ((tell kb1 "~S11 ^ ~S21 ^S12 ^ ~B11 ^ B21 ^ ~B12"))
  "Rules R1 through R4"
  ((tell kb1 "~S11 => ~W11 ^ ~W12 ^ ~W21"))
  ((tell kb1 "~S21 => ~W11 ^ ~W21 ^ ~W22 ^ ~W31"))
  ((tell kb1 "~S12 => ~W11 ^ ~W12 ^ ~W22 ^ ~W13"))
  ((tell kb1 "S12 => W13 | W12 | W22 | W11"))
  "Now the query -- this may take a while."
  ((ask kb1 "W13") *)
  
  "Now a quick demo of the Horn Logic backward chainer."
  ((setf kb2 (make-horn-kb)))
  "Now we define the Member predicate."
  ((tell kb2 "Member(x,Cons(x,y))"))
  ((tell kb2 "Member(x,rest) => Member(x,Cons(y,rest))"))
  ((ask-each kb2 "Member(x,Cons(1,Cons(2,Cons(3,Nil))))" #'print))
  ((ask-patterns kb2 "Member(x,Cons(1,Cons(2,Cons(3,Nil))))" "x") '(1 2 3))
  ((ask-pattern kb2 "Member(x,Cons(1,Cons(2,Cons(3,Nil)))) & x=2" "x") '2)
  ((ask-patterns kb2 "s = Cons(1,Cons(2,Nil))
                        & Member(x,s) & Member(y,s)" '($x $y))
   '((1 1) (1 2) (2 1) (2 2)))
 
  "A family relationships knowledge base and problem."
  ((tell kb2 '(Mother Gerda Peter)))
  ((tell kb2 '(Father Torsten Peter)))
  ((tell kb2 '(Father Peter Isabella)))
  ((tell kb2 '(Father Peter Juliet)))
  ((tell kb2 '(=> (mother $x $y) (parent $x $y))))
  ((tell kb2 '(=> (father $x $y) (parent $x $y))))
  ((tell kb2 '(=> (and (parent $g $p) (parent $p $c)) (grand-parent $g $c))))
  ((ask-patterns kb2 '(grand-parent $x $y)) 
   '((Grand-parent Gerda Isabella) (Grand-parent Gerda Juliet) 
     (Grand-parent Torsten Isabella) (Grand-parent Torsten Juliet)))
  
  "Now the 'Criminal' problem from [p 271-272]."
  ((setf kb3 (make-horn-kb)))
  ((tell kb3 "American(x) ^ Weapon(y) ^ Nation(z) ^ Hostile(z) ^ Sells(x,z,y)
		 => Criminal(x)"))
  ((tell kb3 "Owns(Nono,M1)"))
  ((tell kb3 "Missle(M1)"))
  ((tell kb3 "Owns(Nono,x) ^ Missle(x) => Sells(West,Nono,x)"))
  ((tell kb3 "Missle(x) => Weapon(x)"))
  ((tell kb3 "Enemy(x,America) => Hostile(x)"))
  ((tell kb3 "American(West)"))
  ((tell kb3 "Nation(Nono)"))
  ((tell kb3 "Enemy(Nono,America)"))
  ((tell kb3 "Nation(America)"))
  ((ask kb3 "Criminal(West)") 't)
  ((ask-pattern kb3 "Criminal(x)" "x") 'West)
  
  )