Relation Holds

• Defined in ontology: Kif-relations
• Source pathname: /tmp_mnt/vol/q/htw/cms/ontolingua/examples/kif/../../all-ontologies/kif/kif-relations.lisp

Instance-Of@Frame-Ontology: Relation, Set

Documentation@Ol%Frame-Ontology:

If $tau$ denotes a relation, then the sentence {tt (holds $tau$ $tau_1$ ... $tau_k$)} is true if and only if
the list of objects denoted by $tau_1$,...,$tau_k$ is a member of that relation.

Implication Axioms for Holds:

(=> (Holds ?R @Args) (Member (Listof @Args) ?R))

Equivalence Axioms for Holds:

(<=> (Holds ?R @Args) (And (Relation ?R) (Member (Listof @Args) ?R)))

Axioms for Holds:

(Relation ?R)

(Undefined@Ol-User%Kif-Extensions (Arity@Frame-Ontology Holds))

Implication Axioms mentioning Holds:

(=> (Inverse ?Binary-Relation)
    (<=> (Holds ?Binary-Relation ?X ?Y)
         (Holds (Inverse ?Binary-Relation) ?Y ?X)))

(=> (= (Exact-Domain@Frame-Ontology ?Relation) ?Domain-Relation)
    (Forall (?Tuple @Args)
            (<=> (Holds ?Domain-Relation @Args)
                 (And (Member ?Tuple ?Relation)
                      (= (Listof @Args) (Butlast ?Tuple))))))

(=> (= (Exact-Range@Frame-Ontology ?Relation) ?Range-Class)
    (Forall (?Range-Instance)
            (<=> (Holds ?Range-Class ?Range-Instance)
                 (Exists (?Tuple)
                         (And (Member ?Tuple ?Relation)
                              (= (Last ?Tuple) ?Range-Instance))))))

(=> (= (All-Values@Frame-Ontology ?Instance ?Binary-Relation)
       ?Set-Of-Values)
    (Forall (?Value)
            (<=> (Member ?Value ?Set-Of-Values)
                 (Holds ?Binary-Relation ?Instance ?Value))))

(=> (= (All-Inherited-Slot-Values@Frame-Ontology ?Class
                                  ?Binary-Relation)
       ?Set-Of-Values)
    (Forall (?Instance ?Value)
            (=> (Instance-Of@Frame-Ontology ?Instance ?Class)
                (<=> (Member ?Value ?Set-Of-Values)
                     (Holds ?Binary-Relation ?Instance ?Value)))))

Equivalence Axioms mentioning Holds:

(<=> (Irreflexive-Relation@Frame-Ontology ?R)
     (And (Binary-Relation ?R) (Forall (?X) (Not (Holds ?R ?X ?X)))))

(<=> (Symmetric-Relation@Frame-Ontology ?R)
     (And (Binary-Relation ?R)
          (=> (Holds ?R ?X ?Y) (Holds ?R ?Y ?X))))

(<=> (Total-Order-Relation@Frame-Ontology ?R)
     (And (Partial-Order-Relation@Frame-Ontology ?R)
          (=> (And (Instance-Of@Frame-Ontology 
                       ?X
                       (Exact-Domain@Frame-Ontology ?R))
                   (Instance-Of@Frame-Ontology 
                       ?Y
                       (Exact-Domain@Frame-Ontology ?R)))
              (Or (Holds ?R ?X ?Y) (Holds ?R ?Y ?X)))))

(<=> (Inherited-Through-Class-Of-Relation@Frame-Ontology ?R)
     (And (Binary-Relation ?R)
          (=> (And (Holds ?R ?X ?C1)
                   (Class@Frame-Ontology ?C1)
                   (Class@Frame-Ontology ?C2)
                   (Subclass-Of@Frame-Ontology ?C2 ?C1))
              (Holds ?R ?X ?C2))))

(<=> (Instance-Of@Frame-Ontology ?Individual ?Class)
     (And (Class@Frame-Ontology ?Class) (Holds ?Class ?Individual)))