Theory KIF-RELATIONS

The KIF vocabulary concerning relations and functions.

Theories included by Kif-Relations:

    Kif-Sets
    Kif-Lists
       Kif-Numbers

Theories that include Kif-Relations:

    Frame-Ontology
       Vt-Domain
          Vt-Example
       Configuration-Design
          Vt-Design
             Simple-Bikes
             Vt-Domain ...
       Physical-Quantities
          Unary-Scalar-Functions
             Cml
                Thermodynamics
                Dme
                   Thermodynamics
          Standard-Units
             Simple-Bikes
             Cml ...
             Vt-Design ...
             Unary-Scalar-Functions ...
          Scalar-Quantities
             Vt-Design ...
             Vector-Quantities
       Abstract-Algebra
          Physical-Quantities ...
       Jat-Generic
          Job-Assignment-Task
       Generic-Bibliography
       Slot-Constraint-Sugar
          Generic-Bibliography
    Kif-Ontology

12 classes defined:

    Defined
    Relation
       Function
          One-One
          Many-One
          Unary-Function
          Binary-Function
       Unary-Relation
       Binary-Relation
          One-One
          Many-One
          One-Many
          Many-Many
          Unary-Function
    Undefined

1 relation defined:

9 functions defined:

1 instance defined:

The following constants were used from included theories:

The following constants were used from theories not included:

All constants that were mentioned were defined.

Class RELATION

Subclass-Of: Set
Axioms:
(<=> (Relation ?R) 
     (And (Set ?R) (Forall (?X) (=> (Member ?X ?R) (List ?X)))) )

Class FUNCTION

Subclass-Of: Relation
Axioms:
(<=> (Function ?F) 
     (And (Relation ?F) 
          (Forall (?L ?M) 
                  (=> (Member ?L ?F) 
                      (Member ?M ?F) 
                      (= (Butlast ?L) (Butlast ?M)) 
                      (= (Last ?L) (Last ?M)) ))))

Undefined BOTTOM

The unique object which is the value of functions when applied to arguments on which they are not defined.
Instance-Of: Undefined

Class UNDEFINED

True of terms denoting the bottom object, usually meaning that a function is undefined on given arguments. There is exactly one object in the universe of discourse that is undefined, called BOTTOM. Functional terms that are undefined are equal to this special element.
All-Instances: {Bottom}

Class DEFINED

A term is defined if it does not denote the undefined object, called bottom. (defined (F x)) means that the function F is defined for the object x. (F x) denotes its value. In relational terminology, (defined (F x)) means (exists ?y (F x ?y)).
Axioms:
(<=> (Defined ?X) (Not (Undefined ?X)))

Relation HOLDS

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.
Axioms:
(Undefined (Arity Holds)) 

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

Function VALUE

If $tau$ denotes a function with a value for the objects denoted by $tau_1$,..., $tau_k$, then the term {tt (value $tau$ $tau_1$ ... $tau_k$)} denotes the value of applying that function to the objects denoted by $tau_1$,...,$tau_k$. Otherwise, the value is undefined.
Axioms:
(Undefined (Arity Value)) 

(Undefined (Arity Value))

Function IDENTITY

The value of the identity function is just its argument.
Arity: 2

Function APPLY

Arity: 3
Axioms:
(Nth-Domain Apply 1 Function) 

(<=> (Apply ?F ?List ?Result) 
     (And (Function ?F) 
          (= ?List (Listof @Args)) 
          (Value ?F @Args ?Result) ))

Function MAP

Arity: 3
Axioms:
(= (Map ?F ?List) 
   (If (Null ?List) 
       (Listof) 
       (Cons (Value ?F (First ?List)) (Map ?F (Rest ?List))) ))

Function UNIVERSE

The universe of a relation is the set of all objects occurring in some list contained in that relation.
Arity: 2
Domain: Relation
Axioms:
(<=> (Universe ?R ?Set) 
     (And (Relation ?R) 
          (= (Setofall ?X
                       (Exists (?List) 
                               (And (Member ?List ?R) 
                                    (Item ?X ?List) )))
             ?Set)))

Class UNARY-RELATION

A unary relation is a non-empty relation in which all lists have exactly one item.
Subclass-Of: Relation
Axioms:
(<=> (Unary-Relation ?R) 
     (And (Relation ?R) 
          (Not (Empty ?R)) 
          (Forall (?List) (=> (Member ?List ?R) (Single ?List))) ))

Class BINARY-RELATION

A binary relation is a non-empty relation in which all lists have exactly two items.
Subclass-Of: Relation
Axioms:
(<=> (Binary-Relation ?R) 
     (And (Relation ?R) 
          (Not (Empty ?R)) 
          (Forall (?List) (=> (Member ?List ?R) (Double ?List))) ))

Function INVERSE

The inverse of a binary relation is a binary relation with all tuples reversed.
Arity: 2
Domain: Binary-relation
Axioms:
(<=> (Inverse ?R ?Relation) 
     (And (Binary-Relation ?R) 
          (= (Setofall (Listof ?Y ?X) (Holds ?R ?X ?Y)) ?Relation) ))

Function COMPOSITION

The composition of a binary relation $r_1$ and a binary relation $r_2$ is a binary relation in which an object $x$ is related to an object $z$ if and only if there is an object $y$ such that $x$ is related to $y$ by $r_1$ and $y$ is related to $z$ by $r_2$.
Arity: 3
Axioms:
(Nth-Domain Composition 2 Binary-Relation) 

(Nth-Domain Composition 1 Binary-Relation) 

(<=> (Composition ?R1 ?R2 ?Relation) 
     (And (Binary-Relation ?R1) 
          (Binary-Relation ?R2) 
          (= (Setofall (Listof ?X ?Z) 
                       (Exists (?Y) 
                               (And (Holds ?R1 ?X ?Y) 
                                    (Holds ?R2 ?Y ?Z) )))
             ?Relation)))

Class ONE-ONE

Subclass-Of: Binary-relation, Function

Slots Of Instances:

Inverse:
Slot-Value-Type: Function
Axioms:
(<=> (One-One ?R) 
     (And (Binary-Relation ?R) 
          (Function ?R) 
          (Value-Type ?R Inverse Function) ))

Class MANY-ONE

Subclass-Of: Binary-relation, Function
Axioms:
(<=> (Many-One ?R) (And (Binary-Relation ?R) (Function ?R)))

Class ONE-MANY

Subclass-Of: Binary-relation

Slots Of Instances:

Inverse:
Slot-Value-Type: Function
Axioms:
(<=> (One-Many ?R) 
     (And (Binary-Relation ?R) (Value-Type ?R Inverse Function)) )

Class MANY-MANY

Subclass-Of: Binary-relation
Axioms:
(<=> (Many-Many ?R) 
     (And (Binary-Relation ?R) 
          (Not (Function ?R)) 
          (Not (Function (Inverse ?R))) ))

Class UNARY-FUNCTION

A unary function is a function with a single argument and a single value. Hence, it is also a binary relation.
Subclass-Of: Binary-relation, Function
Axioms:
(<=> (Unary-Function ?F) (And (Function ?F) (Binary-Relation ?F)))

Class BINARY-FUNCTION

A binary function is a function with two arguments and one value. Hence, it is a relation with three arguments.
Subclass-Of: Function
Axioms:
(<=> (Binary-Function ?F) 
     (And (Function ?F) 
          (Not (Empty ?F)) 
          (Forall (?List) (=> (Member ?List ?F) (Triple ?List))) ))

This document was generated using Ontolingua.
Formatting and translation code was written by
François Gerbaux and Tom Gruber