new tests for Modals.java and THFnew.java translation to HOL

tests/TQM3.kif

@@ -0,0 +1,45 @@
+; (note TQM3)
+; (time 20)
+; (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))

tests/TQM3.kif.tq

@@ -0,0 +1,46 @@
+(note TQM3)
+(time 20)
+(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))

tinyHOL.kif

@@ -1,5 +1,6 @@
 (domain modalAttribute 1 Formula)
 (domain modalAttribute 2 NormativeAttribute)
+(instance modalAttribute BinaryPredicate)
 
 (subclass Formula Physical)
 (subclass DeonticAttribute Attribute)
@@ -13,6 +14,10 @@
 (domain knows 1 AutonomousAgent)
 (domain knows 2 Formula)
 
+(instance believes BinaryPredicate)
+(domain believes 1 AutonomousAgent)
+(domain believes 2 Formula)
+
 (instance Bill Human)
 (instance Joe Human)