The KIF vocabulary concerning relations and functions.

**Last modified:***Monday, 13 December 1993***Source code: kif-ontology.lisp****List of other known theories**

Kif-SetsKif-ListsKif-Numbers

Frame-OntologyVt-DomainVt-ExampleConfiguration-DesignVt-DesignSimple-BikesVt-Domain...Physical-QuantitiesUnary-Scalar-FunctionsCmlThermodynamicsDmeThermodynamicsStandard-UnitsSimple-BikesCml...Vt-Design...Unary-Scalar-Functions...Scalar-QuantitiesVt-Design...Vector-QuantitiesAbstract-AlgebraPhysical-Quantities...Jat-GenericJob-Assignment-TaskGeneric-BibliographySlot-Constraint-SugarGeneric-BibliographyKif-Ontology

DefinedRelationFunctionOne-OneMany-OneUnary-FunctionBinary-FunctionUnary-RelationBinary-RelationOne-OneMany-OneOne-ManyMany-ManyUnary-FunctionUndefined

**The following constants were used from included theories:**

**+***defined as a***function***in theory***Kif-Numbers****1+***defined as a***function***in theory***Kif-Numbers****<***defined as a***relation***in theory***Kif-Numbers****=<***defined as a***relation***in theory***Kif-Numbers****Butlast***defined as a***function***in theory***Kif-Lists****Cons***defined as a***function***in theory***Kif-Lists****Double***defined as a***class***in theory***Kif-Lists****Empty***defined as a***class***in theory***Kif-Sets****First***defined as a***function***in theory***Kif-Lists****Integer***defined as a***class***in theory***Kif-Numbers****Item***defined as a***relation***in theory***Kif-Lists****Last***defined as a***function***in theory***Kif-Lists****List***defined as a***class***in theory***Kif-Lists****Member***defined as a***relation***in theory***Kif-Sets****Null***defined as a***class***in theory***Kif-Lists****Rest***defined as a***function***in theory***Kif-Lists****Set***defined as a***class***in theory***Kif-Sets****Single***defined as a***class***in theory***Kif-Lists****Triple***defined as a***class***in theory***Kif-Lists**

**The following constants were used from theories not included:**

**All-Instances***defined as a***function***in theory***Frame-Ontology****Arity***defined as a***function***in theory***Frame-Ontology****Class***defined as a***class***in theory***Frame-Ontology****Documentation***defined as a***relation***in theory***Frame-Ontology****Domain***defined as a***relation***in theory***Frame-Ontology****Exact-Range***defined as a***function***in theory***Frame-Ontology****Nth-Domain***defined as a***relation***in theory***Frame-Ontology****Subclass-Of***defined as a***relation***in theory***Frame-Ontology****Total-On***defined as a***relation***in theory***Frame-Ontology****Value-Type***defined as a***relation***in theory***Frame-Ontology**

**All constants that were mentioned were defined.**

**Subclass-Of:**Set

**Axioms:**

(<=> (Relation ?R) (And (Set ?R) (Forall (?X) (=> (Member ?X ?R) (List ?X)))) )

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp****Also defined in:**Frame-ontology

**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)) ))))

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp****Also defined in:**Frame-ontology

The unique object which is the value of functions when applied to arguments on which they are not defined.

**Instance-Of:**Undefined

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp**

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}

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp**

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)))

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp**

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)))

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp**

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))

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp**

The value of the identity function is just its argument.

**Arity:**2

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp**

**Arity:**3

**Axioms:**

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

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp**

**Arity:**3

**Axioms:**

(= (Map ?F ?List) (If (Null ?List) (Listof) (Cons (Value ?F (First ?List)) (Map ?F (Rest ?List))) ))

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp**

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)))

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp**

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))) ))

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp****Also defined in:**Frame-ontology

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))) ))

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp****Also defined in:**Frame-ontology

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) ))

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp****Also defined in:**Frame-ontology

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)))

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp****Also defined in:**Frame-ontology

**Subclass-Of:**Binary-relation, Function

**Inverse:***Slot-Value-Type:*Function

*Slots Of Instances:*

**Axioms:**

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

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp**

**Subclass-Of:**Binary-relation, Function

**Axioms:**

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

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp**

**Subclass-Of:**Binary-relation

**Inverse:***Slot-Value-Type:*Function

*Slots Of Instances:*

**Axioms:**

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

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp**

**Subclass-Of:**Binary-relation

**Axioms:**

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

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp**

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)))

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp****Also defined in:**Frame-ontology

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))) ))

**Defined in theory: Kif-relations****Source code: kif-ontology.lisp**

Formatting and translation code was written by