(note TQM3)
(time 20)
(minLang thf)
(category modal)
(file tinySUMO.kif)
(file tinyHOL.kif)

;3. Bill believes that the Earth is flat.  Is the Earth flat?  Does Bill know that the Earth is flat?
; if you try to circumnavigate a flat earth you will fall off the edge and die
; Does Bill believe he will die if he tries to circumnavigate the Earth?

(believes Bill (attribute Earth Flat))

; believes has fewer successor worlds than knows
; a quantifier over fewer things is easier, therefore
; the implication is "backwards" from what one would
; expect
    
(=>
  (believes ?H ?F)
  (knows ?H ?F))
        
(=>
  (and
    (instance ?C Circumnavigation)
    (located ?C ?E)
    (attribute ?E Flat)
    (agent ?C ?A))
  (attribute ?A Dead))
     
; We want to say if (X => Y) and A believes X then A believes Y - requires true HOL

(=>
  (and
    (=> ?X ?Y)
    (believes ?A X))
  (believes ?A ?Y))
    
(believes Bill
  (and
    (instance ?C Circumnavigation)
    (located ?C ?E )
    (attribute ?E Flat)
    (agent ?C Joe)))

       
; (believes Bill
;   (attribute ?P Dead))

(query
  (believes Bill
    (attribute Joe Dead)))

(answer yes)