;;;; -*-  Mode: LISP; Syntax: Common-Lisp; Base: 10                        -*-
;;;; -------------------------------------------------------------------------
;;;; File name: quantification-tests.lsp
;;;;    System: Companions
;;;;    Author: Tom Hinrichs
;;;;   Created: November 7, 2003 09:13:21
;;;;   Purpose: test quantification scoping
;;;;  Modified: Wednesday, December 10, 2003 at 13:12:06 by hinrichs
;;;; -------------------------------------------------------------------------

(in-package :cl-user)

(defun trace-quant ()
  #+allegro-ide
  (setf (cg:state (devel::trace-dialog)) :normal)
  (trace fire::do-query fire::query-clause fire::explore-other-terms fire:ask 
         fire::use-single-term-clause fire::applicable-clauses fire::do-quantifier-query
         fire::conj-query fire::do-subquery))

;;; use (fire::show-clause-index (first (fire::clause-indexes fire::*kb*)))
;;; to see contents of clause index.

(defun quantification-test-reasoner (&optional (title "Quantification test")) 
  (unless (fire:open-kb? fire:*kb*)
    (setf fire:*kb* nil)        ;; Clear the clause indexes by creating a new kb
    (fire::make-qrg-darpa-kb)    ;; Set up KB
    (setf fire:*reasoner* nil))
  (unless fire:*reasoner*
    (setq r (fire:make-reasoner title))
    (fire:in-reasoner r))
  (fire::clear-reasoner-clause-indexes)
  (fire::clear-kb-clause-indexes))

;;;
;;; Test simple existential quantification
;;;
(defun test-quantification1 ()
  (quantification-test-reasoner)
  (fire:create-clause-index-from-axioms
   "Quant Test1"
   '((implies (thereExists ?X 
                    (and (isa ?X Foo)
                         (somePred ?X ?Y)))
              (someOtherPred ?Y))))
  (fire:add-clause-index-to-reasoner "Quant Test1" fire:*reasoner*)
  (ltre:assume! '(isa MyFoo Foo) :test-quant1)
  (ltre:assume! '(somePred MyFoo MyBar) :test-quant1))

;;; (fire::query '(someOtherPred MyBar))  ; => t
;;; (fire::query '(someOtherPred MyFoo))  ; => nil
;;; (fire::query '(someOtherPred ?what))  ; => MyBar


;;;
;;; Test double existential quantifiers
;;;
(defun test-quantification2 ()
  (quantification-test-reasoner)
  (fire:create-clause-index-from-axioms
   "Quant Test2"
   '((implies (thereExists ?X
                 (thereExists ?Y
                    (and (isa ?X Foo)
                         (isa ?Y Bar)
                         (somePred ?X ?Y ?Z))))
              (someOtherPred ?Z))))
  (fire:add-clause-index-to-reasoner "Quant Test2" fire:*reasoner*)
  (ltre:assume! '(isa MyFoo Foo) :test-quant2)
  (ltre:assume! '(isa MyBar Bar) :test-quant2)
  (ltre:assume! '(somePred MyFoo MyBar MyBaz) :test-quant2)
  (ltre:assume! '(somePred MyBar MyFoo MyBad) :test-quant2))

;;; (fire::query '(someOtherPred MyBaz)) ; => t
;;; (fire::query '(someOtherPred MyBad)) ; => nil

;;;
;;; Test recursive backchaining on the same quantified rule
;;;
(defun test-quantification3 ()
  (quantification-test-reasoner)
  (fire:create-clause-index-from-axioms
   "Quant Test3"
   '((implies (thereExists ?Y
                 (and (connected ?X ?Y)
                      (connected ?Y ?Z)
                      (different ?X ?Y)   ;; Note: Fire doesn't implement this correctly.
                      (different ?Z ?Y)   ;; (Should be variable arity)
                      (different ?X ?Z)))
              (connected ?X ?Z))))
  (fire:add-clause-index-to-reasoner "Quant Test3" fire:*reasoner*)
  (ltre:assume! '(connected A B) :test-quant3)
  (ltre:assume! '(connected B C) :test-quant3)
  (ltre:assume! '(connected C D) :test-quant3))

;;; (fire::query '(connected A C))  ; simple one level backchaining
;;; (fire::query '(connected A D))  ; This should force backchaining within the rule.
;;; (fire::query '(connected A ?what))

;;;
;;; Test matching against explicitly asserted existential clauses
;;;
(defun test-quantification4 ()
  (quantification-test-reasoner)
  (fire:create-clause-index-from-axioms
   "Quant Test4"
   '((implies (thereExists ?Y
                 (somePredicate ?X ?Y))
              (someObscurePredicate ?X))))
  (fire:add-clause-index-to-reasoner "Quant Test4" fire:*reasoner*)
  (ltre:assume! '(thereExists ?Bar
                               (somePredicate MyFoo ?Bar)) :test-quant4))

;;; (fire::query '(someObscurePredicate MyFoo))  ; => t
;;; (fire::query '(someObscurePredicate MyBar))  ; => nil
;;; (fire::query '(someObscurePredicate ?what))  ; => MyFoo

;;; ------------------------------------------------------------------------
;;; The remaining two *don't* work:

(defun test-quantification5 ()
  (quantification-test-reasoner)
  (fire:create-clause-index-from-axioms
   "Quant Test5"
   '((implies (purposeOfEvent ?EVENT
                 (thereExists ?SIT 
                    (and (genls ?SITTYPE Situation-Temporal)  ; WorldPeace is not an Event, but is a Situation-Temporal
                         (isa ?SIT ?SITTYPE)
                         (startsDuring ?SIT ?EVENT))))        ; argIsa requires a TemporalThing
              (eventToAchievePrimitive-SitType ?EVENT ?SITTYPE))))
  (fire:add-clause-index-to-reasoner "Quant Test5" fire:*reasoner*)
  (ltre:assume! '(isa IraqInvasion MilitaryInvasion) :test-quant5)
  (ltre:assume! '(purposeOfEvent IraqInvasion 
                                  (thereExists ?sit 
                                               (and (genls WorldPeace Situation-Temporal)
                                                    (isa ?sit WorldPeace) 
                                                    (startsDuring ?sit IraqInvasion)))) :test-quant5))

;; (fire::query '(eventToAchievePrimitive-SitType IraqInvasion ?why))
;; (fire::query '(eventToAchievePrimitive-SitType ?what UtopianHallucination))  ;; fails (with timeout?)

;;; Issue:
;;; We know that (genls WorldPeace Situation-Temporal)
;;; and (genls Situation-Temporal TemporalThing)
;;; so this rule deviates from the version in CYC in that it requires ?SIT-TYPE to
;;; be a type of Situation-Temporal instead of Event (which is how it should be anyway)


;;; This fails because the directly asserted existential clause doesn't unify with the
;;; query, even though it should be provable.  This points out the limit of the approach.
;;; In order to make this test work, we would have to canonicalize all the content as it
;;; is entered into the KB, which is what Cyc does.  I'm looking into that now.

;;;
;;; Universally Quantified rules
;;;
(defun test-quantification6 ()
  (quantification-test-reasoner)
  (fire:create-clause-index-from-axioms
   "Quant Test6"
   '((forAll ?MARINE 
      (forAll ?PLAN 
         (implies (and (isa ?MARINE USMarinePersonnel)
                       (isa ?PLAN (PlanningFn MilitaryAttack))
                       (performedBy ?PLAN ?MARINE))
                  (SmartMilitaryOfficer ?MARINE))))))
  (fire:add-clause-index-to-reasoner "Quant Test6" fire:*reasoner*)
  (ltre:assume! '(isa GI-Joe USMarinePersonnel) :test-quant6)
  (ltre:assume! '(isa PlanningAttack001 (PlanningFn MilitaryAttack)) :test-quant6)
  (ltre:assume! '(performedBy PlanningAttack001 GI-Joe) :test-quant6))

;;; (fire::query '(SmartMilitaryOfficer ?who))

;;; This fails because the clause-index creation routine doesn't see the
;;; consequent of the rule, since it's embedded inside the forAll.
;;; This is waiting on correctly implementing the forAll canonicalizer.

(defun test-quantification7 ()
  (quantification-test-reasoner)
  (fire:create-clause-index-from-axioms
   "Quant Test7"
   '((implies (and (isa ?MARINE USArmyPersonnel)
                   (isa ?PLAN (PlanningFn MilitaryAttack)))
              (SmartMilitaryOfficer ?MARINE))))
  (fire:add-clause-index-to-reasoner "Quant Test7" fire:*reasoner*)
  (ltre:assume! '(isa GI-Joe USMarinePersonnel) :test-quant7)
  (ltre:assume! '(isa PlanningAttack001 (PlanningFn MilitaryAttack)) :test-quant7)
  (ltre:assume! '(performedBy PlanningAttack001 GI-Joe) :test-quant7))

#||

;;; Grist for future tests:

(implies (purposeOfPlan ?PLAN
            (thereExists ?SIT 
               (and (genls ?SITTYPE Event) 
                    (isa ?SIT ?SITTYPE) 
                    (implies (executionOfPlan ?PLAN ?EXEC)
                       (startsDuring ?SIT ?EXEC)))))
         (planToAchievePrimitive-SitType ?PLAN ?SITTYPE))

         
(forAll ?CONVEY
        (implies
         (and (isa ?CONVEY ConveyingMaterials)
              (isa ?CONVEY Movement-TranslationEvent)
              (subEvents OperationReliefOrange ?CONVEY)
              (directingAgent ?CONVEY UnitedStatesOfAmerica))
         (likelihood
          (thereExists ?MONITORING
                       (and (isa ?MONITORING Monitoring)
                            (situationMonitored ?MONITORING ?CONVEY)))
          MediumToVeryHigh)))

(implies (and (isa ?x MilitaryUnit)
              (thereExists ?y
                (and (isa ?y MilitaryUnit)
                     (thereExists ?t 
                       (and (isa ?t MilitaryTask)
                            (victim ?t ?x)
                            (performedBy ?t ?y))))))
         (underAttack ?x))


||#

(defun test-kens-case ()
  (quantification-test-reasoner)
  (fire:create-clause-index-from-axioms
   "Ken's Case Test"
   '((implies (and (isa ?x ModernMilitaryUnit-Deployable)
                   (thereExists ?y
                     (and (isa ?y ModernMilitaryUnit-Deployable)
                          (thereExists ?t 
                          (and (isa ?t MilitaryTask)
                               (victim ?t ?x)
                               (performedBy ?t ?y))))))
         (underAttack ?x))))
  (fire:add-clause-index-to-reasoner "Ken's Case Test" fire:*reasoner*)
  (ltre:assume! '(isa Alpha1 ModernMilitaryUnit-Deployable) :kens-case)
  (ltre:assume! '(isa BadGuys ModernMilitaryUnit-Deployable) :kens-case)
  (ltre:assume! '(isa Task1 MilitaryTask) :kens-case)
  (ltre:assume! '(victim Task1 Alpha1) :kens-case)
  (ltre:assume! '(performedBy Task1 BadGuys) :kens-case)
  )


;;; (fire::query '(underAttack Alpha1))





(defun test-quantification-w-cases ()
  (quantification-test-reasoner)
  (fire:create-clause-index-from-axioms
   "Quant Case Test"
   '((implies (thereExists ?X 
                    (and (isa ?X Foo)
                         (somePred ?X ?Y)))
              (someOtherPred ?Y))))
  (fire:add-clause-index-to-reasoner "Quant Case Test" fire:*reasoner*)
  (ltre:assume! '(ist-Information TestCase (isa MyFoo Foo)) :test-quant-cases)
  (ltre:assume! '(ist-Information TestCase (somePred MyFoo MyBar)) :test-quant-cases))

;;; (fire::query '(ist-Information TestCase (someOtherPred MyBar)))  ; => t
;;; (fire::query '(ist-Information TestCase (someOtherPred MyFoo)))  ; => nil
;;; (fire::query '(ist-Information TestCase (someOtherPred ?what)))  ; => MyBar

;;; This fails, partly because applicable-clauses can't find anything.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; End of Code