(domain modalAttribute 1 Formula)
(domain modalAttribute 2 NormativeAttribute)

(subclass Formula Physical)
(subclass DeonticAttribute Attribute)
(instance Obligation DeonticAttribute)
(instance Permission DeonticAttribute)
(instance Prohibition DeonticAttribute)

;; Problem 1

(instance knows BinaryPredicate)
(domain knows 1 AutonomousAgent)
(domain knows 2 Formula)

(instance Bill Human)
(instance Joe Human)

(father Bill Joe)

(instance Jane Human)

(father Bill Jane)

(knows Bill 
  (and
    (father Bill Joe)
    (father Bill Jane)))

; (knows Bill (father Bill Joe))
; thf(conj,conjecture, (( (knows_THFTYPE_IiooI @ lBill_THFTYPE_i @
;  (father_THFTYPE_IiioI @ lBill_THFTYPE_i @ lJoe_THFTYPE_i)) ))).

;; Problem 2


(modalAttribute
  (exists (?BT)
    (and
      (instance ?BT BrushingTeeth)
      (agent ?BT Joe)))
    Obligation)

    ; THF version of above
;  thf(ax49,axiom,((modalAttribute_THFTYPE_IoioI @ (? [BT: $i]:
;    ((instance_THFTYPE_IiioI @ BT @ lBrushingTeeth_THFTYPE_i) &
;    (agent_THFTYPE_IiioI @ BT @ lJoe_THFTYPE_i))) @ lObligation_THFTYPE_i))).

; we have (modalAttribute P Obligation) so we should be able to conclude
;   (not (modalAttribute (not P) Permission)) and also
;   (modalAttribute P Permission)


;------------------------------------------
; SUMO query 1
; (modalAttribute (exists (?BT) (and (instance ?BT BrushingTeeth)
;   (agent ?BT Joe))) Permission))

; THF query 1
;  thf(conj,conjecture,((modalAttribute_THFTYPE_IoioI @ ((? [BT: $i]:
;    ((instance_THFTYPE_IiioI @ BT @ lBrushingTeeth_THFTYPE_i) &
;    (agent_THFTYPE_IiioI @ BT @ lJoe_THFTYPE_i)))) @ lPermission_THFTYPE_i))).
; linear for pasting -
; thf(conj,conjecture,((modalAttribute_THFTYPE_IoioI @ ((? [BT: $i]: ((instance_THFTYPE_IiioI @ BT @ lBrushingTeeth_THFTYPE_i) & (agent_THFTYPE_IiioI @ BT @ lJoe_THFTYPE_i)))) @ lPermission_THFTYPE_i))).
; no proof - don't know why

; it should follow that from

;  thf(ax54,axiom,((! [FORMULA: $i]:
;     ((modalAttribute_THFTYPE_IiioI @ FORMULA @ lObligation_THFTYPE_i) =>
;     (modalAttribute_THFTYPE_IiioI @ FORMULA @ lPermission_THFTYPE_i))))).

; and

;  thf(ax49,axiom,((modalAttribute_THFTYPE_IoioI @ (? [BT: $i]:
;         ((instance_THFTYPE_IiioI @ BT @ lBrushingTeeth_THFTYPE_i) &
;         (agent_THFTYPE_IiioI @ BT @ lJoe_THFTYPE_i))) @ lObligation_THFTYPE_i))).

;  thf(conj,conjecture,((modalAttribute_THFTYPE_IoioI @ (~ (? [BT: $i]:
;    ((instance_THFTYPE_IiioI @ BT @ lBrushingTeeth_THFTYPE_i) &
;    (agent_THFTYPE_IiioI @ BT @ lJoe_THFTYPE_i)))) @ lProhibition_THFTYPE_i))).
; thf(conj,conjecture,(? [V: $i, P : $o] : (~ (modalAttribute_THFTYPE_IoioI @ ~P @ V)))).

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

(=>
  (modalAttribute ?F Necessity)
  (modalAttribute ?F Possibility))