HOLtests.txt

; test problems for SUMO that are beyond first order

; from Transportation.kif
(<=>
    (totalFacilityTypeInArea ?AREA ?TYPE ?COUNT)
    (cardinality
        (KappaFn ?ITEM
            (and
                (instance ?ITEM ?TYPE)
                (located ?ITEM ?AREA))) ?COUNT))
               
(instance DejvickaStation TrainStation)
(located DejvickaStation PragueCzechRepublic)
(instance HradCanskaStation TrainStation)
(located HradCanskaStation PragueCzechRepublic)

Q: (totalFacilityTypeInArea ?AREA ?TYPE ?COUNT)
A: [?AREA=PragueCzechRepublic,?TYPE=TrainStation,?COUNT=2]

; from Merge.kif
; (instance geographicSubregion TransitiveRelation)

; from CountriesAndRegions.kif
; (geographicSubregion PragueCzechRepublic CzechRepublic)

Q: (totalFacilityTypeInArea CzechRepublic ?TYPE ?COUNT)
A: [?TYPE=TrainStation,?COUNT=2]

----------------------------------------------

(believes John
  (acquaintance John Sue))
 
Q: (believes John (acquaintance John ?X))
A: Sue

Q: (believes John (not (acquaintance John Sue)))
A: false

------------

(believes John
  (and
    (acquaintance John Sue)
    (relative John Bill)))
   
Q: (believes John (acquainted John Sue))
A: true

-------------

(instance LastWeek TimePosition)

(holdsDuring LastWeek
  (attribute John Unemployed))
 
Q: (holdsDuring LastWeek
     (exists (?O)
       (employs ?O John)))
A: false
 
(holdsDuring LastWeek
  (attribute John Barefoot)) 
 
Q: (holdsDuring LastWeek
     (exists (?O ?S)
       (and
         (instance ?S Shoe)
         (wears John ?S))))
A: timeout

----------------------------------------------

(exists (?P)
  (and
    (instance ?FM FormalMeeting)
    (agent ?FM John)
    (during ?FM Yesterday)))

Q: (holdsDuring Yesterday
  (attribute John Alone))

A: false

-----------------------------------------------

from SUMO:
(=>
    (and
        (holdsDuring ?T
            (attribute ?H
                (DeadOrMissingBodyPartFn ?P)))
        (instance ?PI ?P)
        (part ?PI ?H)
        (hasPurpose ?PI ?F))
    (not ?F))

(=>
    (instance ?LEG Leg)
    (exists (?ANIMAL)
        (and
            (instance ?ANIMAL Animal)
            (part ?LEG ?ANIMAL))))

(subclass Human Animal)

new:
(instance John Human)

(holdsDuring AfterJohnsInjury
  (attribute John (DeadOrMissingBodyPartFn Leg)))

(=>
  (and
    (instance ?L Leg)
    (part ?L ?H)
    (instance ?H Human)
(hasPurpose ?L
  (exists (?W)
    (and
      (instance ?W Walking)
      (instrument ?W ?L)))

Q: (exists (?W)
       (and
         (instance ?W Walking)
         (during ?W AfterJohnsInjury)
         (agent ?W John)))

A: false

--------------------------------------------

Please note that all these problems should probably be interpreted as "sketches" of problems until we can test them.  They may well be incomplete and we'll have to tackle them on a case-by-case basis to determine, if they don't work, whether the issue is the HOL translator, or just a lack of needed axioms in SUMO