Class Function

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

Subclass-Of@Frame-Ontology: Relation, Set

Superclass-Of@Frame-Ontology:

Binary-Function, Many-One, One-One, Unary-Function, Many-To-One-Relation@Frame-Ontology ...

Has-Instance@Frame-Ontology:

Complement, Difference, Generalized-Intersection, Generalized-Union, Intersection ...

Instance-Of@Frame-Ontology: Class@Frame-Ontology, Relation, Set

Arity@Frame-Ontology: 1

Documentation@Ol%Frame-Ontology:

A function is a mapping from a domain to a range that associates a domain element with exactly one range element. The elements of the domain are tuples, as in relations. The range is a class -- a set of singleton tuples -- and element of the range is an instance of the class. Functions are also first-class objects in the same sense that relations are objects: namely, functions can be viewed as sets of tuples.

Notes:

• Originally defined in the KIF-RELATIONS ontology

---

Slots:

Implication Axioms for Function:

(=> (Function ?Relation)
    (Forall (?Tuple1 ?Tuple2)
            (=> (Member ?Tuple1 ?Relation)
                (Member ?Tuple2 ?Relation)
                (= (Butlast ?Tuple1) (Butlast ?Tuple2))
                (= (Last ?Tuple1) (Last ?Tuple2)))))

Equivalence Axioms for Function:

(<=> (Function ?Relation)
     (And (Relation ?Relation)
          (Forall (?Tuple1 ?Tuple2)
                  (=> (Member ?Tuple1 ?Relation)
                      (Member ?Tuple2 ?Relation)
                      (= (Butlast ?Tuple1) (Butlast ?Tuple2))
                      (= (Last ?Tuple1) (Last ?Tuple2))))))

Frame References to Function:

In class@frame-ontology One-To-Many-Relation@Frame-Ontology:

Slots:

Inverse:

Slot-Value-Type@Frame-Ontology: Function

In class@frame-ontology One-To-One-Relation@Frame-Ontology:

Slots:

Inverse:

Slot-Value-Type@Frame-Ontology: Function

In class@frame-ontology One-Many:

Slots:

Inverse:

Slot-Value-Type@Frame-Ontology: Function

In class@frame-ontology One-One:

Slots:

Inverse:

Slot-Value-Type@Frame-Ontology: Function

Implication Axioms mentioning Function:

(=> (One-One ?R) (Function ?R))

(=> (Many-One ?R) (Function ?R))

(=> (Many-Many ?R) (Not (Function (Inverse ?R))))

(=> (Many-Many ?R) (Not (Function ?R)))

(=> (Unary-Function ?F) (Function ?F))

Equivalence Axioms mentioning Function:

(<=> (One-One ?R)
     (And (Binary-Relation ?R)
          (Function ?R)
          (Value-Type@Frame-Ontology ?R Inverse Function)
          (Value-Cardinality@Frame-Ontology ?R Inverse 1)))

(<=> (Many-One ?R) (And (Binary-Relation ?R) (Function ?R)))

(<=> (One-Many ?R)
     (And (Binary-Relation ?R)
          (Value-Type@Frame-Ontology ?R Inverse Function)
          (Value-Cardinality@Frame-Ontology ?R Inverse 1)))

(<=> (Many-Many ?R)
     (And (Binary-Relation ?R)
          (Not (Function ?R))
          (Not (Function (Inverse ?R)))))

(<=> (Unary-Function ?F) (And (Function ?F) (Binary-Relation ?F)))