# Theory KIF-LISTS

The KIF vocabulary for lists as defined in the KIF 3.0 specification.

### Theories included by Kif-Lists:

`    Kif-Numbers`

### Theories that include Kif-Lists:

```    Kif-Ontology
Kif-Meta
Configuration-Design
Vt-Design
Simple-Bikes
Vt-Domain
Vt-Example
Kif-Ontology
Kif-Relations
Frame-Ontology
Vt-Domain ...
Configuration-Design ...
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```

### 6 classes defined:

```    List
Null
Single
Double
Triple
String```

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

A list is a sequence --- an ordered bag --- of elements. It is KIF primitive.

## Class NULL

True of the list with no items.
Subclass-Of: List

Slots Of Instances:

Length: 0
Axioms:
```(<=> (Null ?List) (And (List ?List) (= (Length ?List) 0)))

```

## Null NIL

The list with no items, of length 0. All null lists are equal to this object, called NIL.
Instance-Of: Null

## Function LISTOF

LISTOF is the sequence constructor function for KIF. It takes any finite number of arguments and denotes the list (i.e., sequence, tuple) of those items.

LISTOF is an operator in KIF.

Range: List
Axioms:
```(Undefined (Arity Listof))

```

## Class SINGLE

A list of length 1.
Subclass-Of: List

Slots Of Instances:

Length: 1
Axioms:
```(<=> (Single ?List) (And (List ?List) (= (Length ?List) 1)))

```

## Class DOUBLE

A list of length 2.
Subclass-Of: List

Slots Of Instances:

Length: 2
Axioms:
```(<=> (Double ?List) (And (List ?List) (= (Length ?List) 2)))

```

## Class TRIPLE

A list of length 3.
Subclass-Of: List

Slots Of Instances:

Length: 3
Axioms:
```(<=> (Triple ?List) (And (List ?List) (= (Length ?List) 3)))

```

## Function FIRST

Arity: 2
Domain: List
Axioms:
```(<=> (First ?List ?Result)
(And (Exists (@Items) (= (Listof ?X @Items) ?List))
(= ?X ?Result) ))

```

## Function SECOND

the SECOND of a list is the second item in the list. It is undefined if the length of the list is not at least 2.
Arity: 2
Domain: List
Axioms:
```(= (Second ?List) (First (Rest ?List)))

```

## Function REST

Arity: 2
Axioms:
```(<=> (Rest ?List ?Rest-List)
(Or (And (Null ?List) (= ?Rest-List ?List))
(Exists (?X @Items)
(And (= ?List (Listof ?X @Items))
(= ?Rest-List (Listof @Items)) ))))

```

## Function LAST

Arity: 2
Domain: List
Axioms:
```(= (Last ?List)
(Cond ((Null ?List) Bottom)
((Null (Rest ?List)) (First ?List))
(True (Last (Rest ?List))) ))

```

## Function BUTLAST

Arity: 2
Axioms:
```(= (Butlast ?List)
(Cond ((Null ?List) Bottom)
((Null (Rest ?List)) Nil)
(True (Cons (First ?List) (Butlast (Rest ?List)))) ))

```

## Relation ITEM

The sentence {tt (item \$tau_1\$ \$tau_2\$)} is true if and only if the object denoted by \$tau_2\$ is a non-empty list and the object denoted by \$tau_1\$ is either the first item of that list or an item in the rest of the list.
Arity: 2
Range: List
Axioms:
```(=> (Item ?X ?List)
(And (Not (Null ?List))
(Or (= ?X (First ?List)) (Item ?X (Rest ?List))) ))

```

## Relation SUBLIST

The sentence {tt (sublist \$tau_1\$ \$tau_2\$)} is true if and only if the object denoted by \$tau_1\$ is a final segment of the list denoted by \$tau_2\$.
Arity: 2
Domain: List
Range: List
Axioms:
```(=> (Sublist ?L1 ?L2) (Or (= ?L1 ?L2) (Sublist ?L1 (Rest ?L2))))

```

## Function CONS

The function {tt cons} adds the object specified as its first argument to the front of the list specified as its second argument.
Arity: 3
Axioms:
```(Nth-Domain Cons 3 List)

(Nth-Domain Cons 2 List)

(<=> (Cons ?X ?List ?New-List)
(And (= ?List (Listof @L)) (= (Listof ?X @L) ?New-List)) )

```

## Function APPEND

The function {tt append} adds the items in the list specified as its first argument to the list specified as its second argument. .
Arity: 3
Axioms:
```(Nth-Domain Append 3 List)

(Nth-Domain Append 2 List)

(Nth-Domain Append 1 List)

(= (Append ?L1 ?L2)
(If (Null ?L1)
(If (List ?L2) ?L2)
(Cons (First ?L1) (Append (Rest ?L1) ?L2)) ))

```

## Function REVAPPEND

The function {tt revappend} is similar to append, except that it adds the items in reverse order.
Arity: 3
Axioms:
```(Nth-Domain Revappend 3 List)

(Nth-Domain Revappend 2 List)

(Nth-Domain Revappend 1 List)

(= (Revappend ?L1 ?L2)
(If (Null ?L1)
(If (List ?L2) ?L2)
(Revappend (Rest ?L1) (Cons (First ?L1) ?L2)) ))

```

## Function REVERSE

The function {tt reverse} produces a list in which the order of items is the reverse of that in the list supplied as its single argument.
Arity: 2
Domain: List
Range: List
Axioms:
```(= (Reverse ?List) (Revappend ?List (Listof)))

```

The functions {tt adjoin} and {tt remove} construct lists by adding or removing objects from the lists specified as their arguments.
Arity: 3
Axioms:
```(Nth-Domain Adjoin 3 List)

(= (Adjoin ?X ?List) (If (Item ?X ?List) ?List (Cons ?X ?List)))

```

## Function REMOVE

The functions {tt adjoin} and {tt remove} construct lists by adding or removing objects from the lists specified as their arguments.
Arity: 3
Axioms:
```(Nth-Domain Remove 3 List)

(Nth-Domain Remove 2 List)

(= (Remove ?X ?List)
(Cond ((Null ?List) Nil)
((And (= ?X (First ?List)) (List ?List))
(Remove ?X (Rest ?List)) )
((List ?List) (Cons ?X (Remove ?X (Rest ?List)))) ))

```

## Function SUBST

The value of {tt subst} is the object or list obtained by substituting the object supplied as first argument for all occurrences of the object supplied as second argument in the object or list supplied as third argument.
Arity: 4
Axioms:
```(= (Subst ?X ?Y ?Z)
(Cond ((= ?Y ?Z) ?X)
((Null ?Z) Nil)
((List ?Z)
(Cons (Subst ?X ?Y (First ?Z)) (Subst ?X ?Y (Rest ?Z))) )
(True ?Z) ))

```

## Function LENGTH

The function constant {tt length} gives the number of items in a list.
Arity: 2
Domain: List
Range: Nonnegative-integer
Axioms:
```(= (Length ?List)
(Cond ((Null ?List) 0) ((List ?List) (1+ (Length (Rest ?List))))) )

```

## Function NTH

{tt nth} returns the item in the list specified as its first
argument in the position specified as its second argument.
Arity: 3
Axioms:
```(Nth-Domain Nth 2 Natural)

(Nth-Domain Nth 1 List)

(= (Nth ?List ?N)
(Cond ((= ?N 1) (First ?List))
((Positive ?N) (Nth (Rest ?List) (1- ?N))) ))

```

## Function NTHREST

{tt nthrest} returns the list specified as its first argument
minus the first \$n\$ items, where \$n\$ is the number specified as its second argument.
Arity: 3
Axioms:
```(Nth-Domain Nthrest 3 List)

(Nth-Domain Nthrest 2 Natural)

(Nth-Domain Nthrest 1 List)

(= (Nthrest ?List ?N) (Cond (True Bottom)))

```

## Class STRING

A string is a sequence of characters.
Subclass-Of: List

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