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

1 relation defined:

5 functions defined:

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