;; copyright Infosys 2019
;; author - Adam Pease - adam.pease@infosys.com

;; Access to and use of these products is governed by the GNU General Public
;; License <http://www.gnu.org/copyleft/gpl.html>.
;; By using these products, you agree to be bound by the terms
;; of the GPL.

;; experiments in higher order logic

;; fanciful test case problem of my Mom tells me to brush my teeth

;; from SUMO - call it SUMO1
(=>
  (modalAttribute ?FORMULA Obligation)
  (not
    (modalAttribute
      (not ?FORMULA) Permission)))

(=>
  (modalAttribute ?FORMULA Permission)
  (not
    (modalAttribute
      (not ?FORMULA) Obligation)))

(subclass Cleaning Process)
(subclass BrushingTeeth Cleaning)
(documentation BrushingTeeth EnglishLanguage "&%Cleaning several instances
of a &%Tooth of an &%Animal a &%Toothbrush.")

(=>
  (instance ?BT BrushingTeeth)
  (exists (?T ?TB ?A)
    (and
      (instance ?A Animal)
      (instance ?TB ToothBrush)
      (instance ?T Tooth)
      (part ?T ?A)
      (instrument ?BT ?TB)
      (destination ?BT ?T))))

;; Prob1
(confersObligation
  (=>
      (instance ?D Day)
      (exists (?BT)
        (and
          (instance ?BT BrushingTeeth)
          (during ?BT (WhenFn ?D))
          (agent ?BT Me))))
  MyMom Me)

;; Prob2
(hasAuthorityOver MyMom Me)

;; from SUMO
;; call it SUMO2
(=>
    (confersObligation ?FORMULA ?AGENT1 ?AGENT2)
    (holdsObligation ?FORMULA ?AGENT2))

;; Prob3a
(=>
  (holdsDuring ?T
    (and
      (hasAuthorityOver ?AUTH ?AG)
      (confersObligation ?F ?AUTH ?AG)))
  (holdsDuring ?T
    (desires ?AG ?F)))

;; Prob3b
(=>
  (and
    (hasAuthorityOver ?AUTH ?AG)
    (confersObligation (holdsDuring ?T ?F) ?AUTH ?AG))
  (desires ?AG (holdsDuring ?T ?F)))

;; Prob3c
(=>
  (and
    (hasAuthorityOverT ?T ?AUTH ?AG)
    (confersObligationT ?T ?F ?AUTH ?AG))
  (desiresT ?T ?AG ?F))

;; Prob3d
(=>
  (and
    (hasAuthorityOver ?AUTH ?AG)
    (confersObligation ?F ?AUTH ?AG))
  (desires ?AG ?F))

;; Prob4
(=>
  (holdsObligation ?F ?AG)
  (modalAttribute ?F Obligation))

;; Prob5
(holdsRight
  (exists (?D)
    (not
      (exists (?BT)
        (and
          (instance ?BT BrushingTeeth)
          (during ?BT (WhenFn ?D))
          (agent ?BT Me)))))
  Me)

;; Todo: describe worlds and acc relns and then give
;; Kripki style translation to FO
;; AP- cool!

(=>
    (modalAttribute ?FORMULA Obligation)
    (modalAttribute ?FORMULA Permission))