;; This file contains general axioms that are used by the TQs. ;; Accordingly, it should be loaded before any of the TQ files. (=> (instance ?REL SymmetricRelation) (forall (?INST1 ?INST2) (=> (holds ?REL ?INST1 ?INST2) (holds ?REL ?INST2 ?INST1)))) (=> (instance ?REL TransitiveRelation) (forall (?INST1 ?INST2 ?INST3) (=> (and (holds ?REL ?INST1 ?INST2) (holds ?REL ?INST2 ?INST3)) (holds ?REL ?INST1 ?INST3)))) (=> (inverse ?REL1 ?REL2) (forall (?INST1 ?INST2) (<=> (holds ?REL1 ?INST1 ?INST2) (holds ?REL2 ?INST2 ?INST1)))) (=> (and (subrelation ?REL1 ?REL2) (holds ?REL1 ?INST1 ?INST2)) (holds ?REL2 ?INST1 ?INST2)) (=> (and (subrelation ?REL1 ?REL2) (holds ?REL1 ?INST1 ?INST2 ?INST3)) (holds ?REL2 ?INST1 ?INST2 ?INST3)) (=> (and (instance ?INST ?CLASS1) (subclass ?CLASS1 ?CLASS2)) (instance ?INST ?CLASS2)) ;; The following axiom is not needed. One should simply declare that "inRegion" is a ;; 'ReflexiveRelation' or, better, use the SUMO relation 'located', which is already ;; asserted to be a 'ReflexiveRelation'. ;;(=> ;; (instance ?X Country) ;; (inRegion ?X ?X)) ;; The following axioms are a short-term workaround for Vampire's apparent inability to ;; respond correctly to queries that involve a "look-up" of an equality assertion. (instance equalSuper BinaryPredicate) (instance equalSuper EquivalenceRelation) (instance equalSuper RelationExtendedToQuantities) (domain equalSuper 1 Entity) (domain equalSuper 2 Entity) (documentation equalSuper "This is not a SUMO term. It is a temporary term, which is intended to cover directly asserted cases of the equality operator, equalAsserted, and cases which are reached by inference, &%equal.") (subrelation equal equalSuper) (subrelation equalAsserted equalSuper) (=> (equalSuper ?ENTITY1 ?ENTITY2) (or (equal ?ENTITY1 ?ENTITY2) (equalAsserted ?ENTITY1 ?ENTITY2)))