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