# Theory KIF-META

The KIF vocabulary for representing metalinguistic knowledge.

### Theories included by Kif-Meta:

```    Kif-Sets
Kif-Lists
Kif-Numbers```

### Theories that include Kif-Meta:

```    Configuration-Design
Vt-Design
Simple-Bikes
Vt-Domain
Vt-Example
Kif-Ontology```

### 36 classes defined:

```    Conjunction
Disjunction
Equation
Equivalence
Expression
Word
Variable
Indvar
Seqvar
Operator
Termop
Sentop
Ruleop
Defop
Constant
Funconst
Relconst
Objconst
Sentence
Logconst
Logsent
Truth
Analytic-Truth
Implication
Inequality
Logterm
Negation
Quanterm
Quantsent
Relsent
Reverse-Implication
Term
Funterm
Listterm
Setterm
Quoterm```

### No instances 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 EXPRESSION

KIF expression is either a word or a list of expressions.
Axioms:
```(<=> (Expression ?Expr)
(Or (Word ?Expr)
(And (List ?Expr)
(Forall (?Subexpr)
(=> (Item ?Subexpr ?Expr)
(Expression ?Subexpr) )))))

```

## Class WORD

An atom in a KIF expression.
Subclass-Of: Expression
Exhaustive-Subclass-Partition: {Variable, Operator, Constant}
Axioms:
```(=> (Word ?Expr) (Not (List ?Expr)))

```

## Class VARIABLE

KIF variable
Subclass-Of: Word
Exhaustive-Subclass-Partition: {Indvar, Seqvar}

## Class OPERATOR

KIF operator
Subclass-Of: Word
Exhaustive-Subclass-Partition: {
Termop, Sentop, Ruleop, Defop}

## Class CONSTANT

A constant used in a KIF expression.
Subclass-Of: Word
Exhaustive-Subclass-Partition: {Funconst, Relconst, Objconst}

## Class FUNCONST

A symbol that denotes a function. Used as the functor of a term expression.
Subclass-Of: Constant

## Class RELCONST

A symbol that denotes a relation (may also be a function). Cannot be used as a functor of a term expression, even if it denotes a function.
Subclass-Of: Constant

## Class OBJCONST

A symbol that denotes a KIF object other than a relation.
Subclass-Of: Constant

## Class INDVAR

An individual variable in a KIF expression. For every individual variable \$nu\$, there is an axiom asserting that it is indeed an individual variable. Each such axiom is a defining axiom for the {tt indvar} relation.
Subclass-Of: Variable

## Class SEQVAR

A sequence variable in a KIF expression. For every sequence variable \$omega\$, there is an axiom asserting that it is a sequence variable. Each such axiom is a defining axiom for the {tt seqvar} relation.
Subclass-Of: Variable

## Class TERMOP

KIF term operator
Subclass-Of: Operator
All-Instances: {
'Quote, 'Listof, 'Cond, 'The, 'Setof, 'Setofall, 'Kappa, 'Lambda}
Axioms:
```(<=> (Termop ?Expr) (Operator ?Expr))

```

## Class SENTOP

KIF sentence operator
Subclass-Of: Operator
All-Instances: {
'Not, 'And, 'Or, '=>, '<=, '<=>, 'Forall, 'Exists}
Axioms:
```(<=> (Sentop ?Expr) (Operator ?Expr))

```

## Class RULEOP

KIF rule operator
Subclass-Of: Operator
All-Instances: {'=>>, '<<=}
Axioms:
```(<=> (Ruleop ?Expr) (Operator ?Expr))

```

## Class DEFOP

KIF definitional operator
Subclass-Of: Operator
All-Instances: {
'Defobject, 'Define-function, 'Defrelation, '=, '=>, 'Axiom, 'Conservative-axiom}
Axioms:
```(<=> (Defop ?Expr) (Operator ?Expr))

```

## Class TERM

KIF term expression
Alias: Expression
Exhaustive-Subclass-Partition: {
Variable, Constant, Listterm, Setterm, Quoterm, Logterm, Quanterm}

## Class FUNTERM

KIF function term expression.
Subclass-Of: List, Term

Slots Of Instances:

First:
Slot-Value-Type: Funconst
Axioms:
```(<=> (Funterm ?Expr)
(And (Term ?Expr)
(List ?Expr)
(Value-Type ?Expr First Funconst) ))

```

## Class LISTTERM

KIF list term expression
Subclass-Of: List, Term
Axioms:
```(<=> (Listterm ?Expr)
(And (Term ?Expr) (List ?Expr) (= (First ?Expr) (Quote Listof))) )

```

## Class SETTERM

KIF set term expression
Subclass-Of: List, Term
Axioms:
```(<=> (Setterm ?Expr)
(And (Term ?Expr) (List ?Expr) (= (First ?Expr) (Quote Setof))) )

```

## Class QUOTERM

KIF quoted term expression.
Subclass-Of: List, Term
Axioms:
```(<=> (Quoterm ?Expr)
(And (Term ?Expr)
(List ?Expr)
(= (First ?Expr) (Quote Quote))
(Expression (First (First ?Expr))) ))

```

## Class LOGTERM

Subclass-Of: Term
Axioms:
```(<=> (Logterm ?X)
(Or (Exists (?P1 ?T1)
(And (Sentence ?P1)
(Term ?T1)
(= ?X (Listof (Quote If) ?P1 ?T1)) ))
(Exists (?P1 ?T1 ?T2)
(And (Sentence ?P1)
(Term ?T1)
(Term ?T2)
(= ?X (Listof (Quote If) ?P1 ?T1 ?T2)) ))
(Exists (?Clist)
(And (List ?Clist)
(=> (Item ?C ?Clist)
(Exists (?P ?T)
(And (Sentence ?P)
(Term ?T)
(= ?C (Listof ?P ?T)) )))
(= ?X (Cons (Quote Cond) ?Clist)) ))))

```

## Class QUANTERM

Subclass-Of: Term
Axioms:
```(<=> (Quanterm ?X)
(Or (Exists (?T ?P)
(And (Term ?T)
(Sentence ?P)
(= ?X (Listof (Quote The) ?T ?P)) ))
(Exists (?T ?P)
(And (Term ?T)
(Sentence ?P)
(= ?X (Listof (Quote Setof) ?T ?P)) ))
(Exists (?Vlist ?P)
(And (List ?Vlist)
(Sentence ?P)
(>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlistp) (Indvar ?V))
(= ?X (Listof (Quote Kappa) ?Vlistp ?P)) ))
(Exists (?Vlist ?Sv ?P)
(And (List ?Vlist)
(Seqvar ?Sv)
(Sentence ?P)
(=> (Item ?V ?Vlist) (Indvar ?V))
(= ?X
(Listof 'Kappa
(Append ?Vlist (Listof ?Sv))
?P))))
(Exists (?Vlist ?T)
(And (List ?Vlist)
(Term ?T)
(>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlistp) (Indvar ?V))
(= ?X (Listof (Quote Lambda) ?Vlistp ?T)) ))
(Exists (?Vlist ?Sv ?T)
(And (List ?Vlist)
(Seqvar ?Sv)
(Sentence ?T)
(=> (Item ?V ?Vlist) (Indvar ?V))
(= ?X
(Listof 'Lambda
(Append ?Vlist (Listof ?Sv))
?T))))))

```

## Class SENTENCE

KIF sentence expression. Has a truth value.
Subclass-Of: Expression
Exhaustive-Subclass-Partition: {
Logconst, Relsent, Equation, Inequality, Logsent, Quantsent}

## Class LOGCONST

A KIF logical constant.
Subclass-Of: Sentence

## Class RELSENT

Subclass-Of: Sentence
Axioms:
```(<=> (Relsent ?X)
(Exists (?R ?Tlist)
(And (Or (Relconst ?R) (Funconst ?R))
(List ?Tlist)
(>= (Length ?Tlist) 1)
(=> (Item ?T ?Tlist) (Term ?T))
(= ?X (Cons ?R ?Tlist)) )))

```

## Class EQUATION

Subclass-Of: Sentence
Axioms:
```(<=> (Equation ?X)
(Exists (?T1 ?T2)
(And (Term ?T1)
(Term ?T2)
(= ?X (Listof (Quote =) ?T1 ?T2)) )))

```

## Class INEQUALITY

Subclass-Of: Sentence
Axioms:
```(<=> (Inequality ?X)
(Exists (?T1 ?T2)
(And (Term ?T1)
(Term ?T2)
(= ?X (Listof (Quote /=) ?T1 ?T2)) )))

```

## Class LOGSENT

KIF logical sentence.
Subclass-Of: Sentence
Exhaustive-Subclass-Partition: {
Negation, Conjunction, Disjunction, Implication, Reverse-implication, Equivalence}

## Class NEGATION

Subclass-Of: Logsent
Axioms:
```(<=> (Negation ?X)
(Exists (?P) (And (Sentence ?P) (= ?X (Listof (Quote Not) ?P)))) )

```

## Class CONJUNCTION

Subclass-Of: Logsent
Axioms:
```(<=> (Conjunction ?X)
(Exists (?Plist)
(And (List ?Plist)
(>= (Length ?Plist) 1)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons (Quote And) ?Plist)) )))

```

## Class DISJUNCTION

Subclass-Of: Logsent
Axioms:
```(<=> (Disjunction ?X)
(Exists (?Plist)
(And (List ?Plist)
(>= (Length ?Plist) 1)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons (Quote Or) ?Plist)) )))

```

## Class IMPLICATION

Subclass-Of: Logsent
Axioms:
```(<=> (Implication ?X)
(Exists (?Plist)
(And (List ?Plist)
(>= (Length ?Plist) 2)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons (Quote =>) ?Plist)) )))

```

## Class REVERSE-IMPLICATION

Subclass-Of: Logsent
Axioms:
```(<=> (Reverse-Implication ?X)
(Exists (?Plist)
(And (List ?Plist)
(>= (Length ?Plist) 2)
(=> (Item ?P ?Plist) (Sentence ?P))
(= ?X (Cons (Quote <=) ?Plist)) )))

```

## Class EQUIVALENCE

Subclass-Of: Logsent
Axioms:
```(<=> (Equivalence ?X)
(Exists (?P1 ?P2)
(And (Sentence ?P1)
(Sentence ?P2)
(= ?X (Listof (Quote <=>) ?P1 ?P2)) )))

```

## Class QUANTSENT

Subclass-Of: Sentence
Axioms:
```(<=> (Quantsent ?X)
(Or (Exists (?V ?P)
(And (Indvar ?V)
(Sentence ?P)
(Or (= ?X (Listof (Quote Forall) ?V ?P))
(= ?X (Listof (Quote Exists) ?V ?P)) )))
(Exists (?Vlist ?P)
(And (List ?Vlist)
(Sentence ?P)
(>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlist) (Indvar ?V))
(Or (= ?X (Listof (Quote Forall) ?Vlist ?P))
(= ?X (Listof (Quote Exists) ?Vlist ?P)) )))))

```

## Function DENOTATION

The term {tt (denotation \$tau\$)} denotes the object denoted by the object denoted by \$tau\$. A quotation denotes the quoted expression; the denotation of any other object is \$bot\$.
Arity: 2

## Function NAME

The term {tt (name \$tau\$)} denotes the standard name for the object denoted by the term \$tau\$. The standard name for an expression \$tau\$ is {tt (quote \$tau\$)}; the standard name for a non-expression is at the
discretion of the user. (Note that there are only a countable number of terms in KIF, but there can be models with uncountable cardinality; consequently, it is not always possible for every object in the universe of discourse to have a unique name.)
Arity: 2

## Class TRUTH

A level-crossing relation used to state that a sentence is true.
Subclass-Of: Sentence

## Relation DEFINING-AXIOM

a defining axiom for a constant is a sentence that helps define the constant. See the KIF specification for details.
Arity: 2
Domain: Constant
Range: Sentence

## Class ANALYTIC-TRUTH

Given a knowledge base \$Delta\$, the sentence {tt (analytic-truth '\$phi\$)} means that the sentence \$phi\$ is logically entailed by the defining axioms of the definitions in knowledge base \$Delta\$.
Subclass-Of: Sentence

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