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
             Job-Assignment-Task
          Generic-Bibliography
          Slot-Constraint-Sugar
             Generic-Bibliography
       Kif-Ontology

6 classes defined:

    List
       Null
       Single
       Double
       Triple
       String

2 relations defined:

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

Function ADJOIN

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) 

(Nth-Domain Adjoin 2 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