In order to facilitate the encoding of knowledge about KIF, the language includes type relations for the various syntactic categories defined in chapter 2.

For every individual variable , there is an axiom asserting that it is
indeed an individual variable. Each such axiom is a defining axiom for the
`indvar` relation.

`(indvar (quote ))`

For every sequence variable , there is an axiom asserting that it is a
sequence variable. Each such axiom is a defining axiom for the `seqvar`
relation.

`(seqvar (quote ))`

`(defrelation termop (?x) :=`

` (member ?x (setof 'quote 'if 'cond 'the 'setof`

` 'kappa 'lambda)))`

`(defrelation sentop (?x) :=`

` (member ?x (setof 'not 'and 'or '=> '<= '<=> 'forall 'exists)))`

`(defrelation ruleop (?x) := (member ?x (setof '=>> '<<=)))`

`(defrelation defop (?x) :=`

` (member ?x (setof 'defobject 'deffunction 'defrelation ':=`

` ':=> ':axiom ':conservative-axiom)))`

For every constant , there is an axiom asserting that it is a
constant. Each such axiom is a defining axiom for the `constant`
relation. The category of each constant is determined from its definition
and/or the uses of the constant in a knowledge base.

`(defrelation constant (constant (quote $\sigma$)))`

From these basic vocabulary items, we define variables, operators, words, and expressions.

`(defrelation variable (?x) := (or (indvar ?x) (seqvar ?x)))`

`(defrelation operator (?x) :=`

` (or (termop ?x) (sentop ?x) (ruleop ?x) (defop ?x)))`

`(defrelation word (?x) :=`

` (or (variable ?x) (operator ?x) (constant ?x)))`

`(defrelation expression (?x) :=`

` (or (word ?x)`

` (and (list ?x)`

` (forall (?y) (=> (item ?y ?x) (expression ?y))))))`

The sentence `(term )` is true if and only if the
object denoted by is a term, i.e. it is either a constant, a
variable, functional term, a list term, a set term, a quoted term, a logical
term, or a quantified term.

`(defrelation term (?x) :=`

` (or (indvar ?x) (objconst ?x) (funconst ?x) (relconst ?x)`

` (funterm ?x) (listterm ?x) (setterm ?x) (quoterm ?x)`

` (logterm ?x) (quanterm ?x)))`

`(defrelation funterm (?x) :=`

` (exists (?f ?tlist)`

` (and (funconst ?f)`

` (list ?tlist)`

` (=> (item ?t ?tlist) (term ?t))`

` (= ?x (cons ?f ?tlist)))))`

`(defrelation listterm (?x) :=`

` (exists ?tlist`

` (and (list ?tlist)`

` (=> (item ?t ?tlist) (term ?t))`

` (= ?x (cons 'listof ?tlist)))))`

`(defrelation setterm (?x) :=`

` (exists ?tlist`

` (and (list ?tlist)`

` (=> (item ?t ?tlist) (term ?t))`

` (= ?x (cons 'setof ?tlist)))))`

`(defrelation (?x) :=`

` (exists (?e)`

` (and (expression ?e)`

` (= ?x `(quote ,?e)))))`

`(defrelation logterm (?x) :=`

` (or (exists (?p1 ?t1)`

` (and (sentence ?p1) (term ?t1) (= ?x `(if ,?p1 ,?t1))))`

` (exists (?p1 ?t1 ?t2)`

` (and (sentence ?p1)`

` (term ?t1)`

` (term ?t2)`

` (= ?x `(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 'cond ?clist))))))`

`(defrelation quanterm (?x) :=`

` (or (exists (?t ?p)`

` (and (term ?t) (sentence ?p)`

` (= ?x (listof 'the ?t ?p))))`

` (exists (?t ?p)`

` (and (term ?t) (sentence ?p)`

` (= ?x (listof 'setof ?t ?p))))`

` (exists (?vlist ?p)`

` (and (list ?vlist) (sentence ?p)`

` (>= (length ?vlist) 1)`

` (=> (item ?v ?vlistp) (indvar ?v))`

` (= ?x (listof '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 '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))))))`

The sentence `(sentence )` is true if and only if the
object denoted by is a sentence, i.e. it is either a logical
constant, a relational sentence, a logical sentence, or a quantified
sentence.

`(defrelation sentence (?x) :=`

` (or (logconst ?x) (relsent ?x) (equation ?x)`

` (inequality ?x) (logsent ?x) (quantsent ?x)))`

`(defrelation 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)))))`

`(defrelation equation (?x) :=`

` (exists (?t1 ?t2)`

` (and (term ?t1) (term ?t2)`

` (= ?x `(= ,?t1 ,?t2)))))`

`(defrelation inequality (?x) :=`

` (exists (?t1 ?t2)`

` (and (term ?t1) (term ?t2)`

` (= ?x `(/= ,?t1 ,?t2)))))`

`(defrelation logsent (?x) :=`

` (or (negation ?x) (conjunction ?x) (disjunction ?x)`

` (implication ?x) (reverse-implication ?x)`

` (equivalence ?x)))`

`(defrelation negation (?x) :=`

` (exists (?p)`

` (and (sentence ?p)`

` (= ?x `(not ,?p)))))`

`(defrelation conjunction (?x) :=`

` (exists ?plist`

` (and (list ?plist)`

` (>= (length ?plist) 1)`

` (=> (item ?p ?plist) (sentence ?p))`

` (= ?x (cons 'and ?plist)))))`

`(defrelation disjunction (?x) :=`

` (exists ?plist`

` (and (list ?plist)`

` (>= (length ?plist) 1)`

` (=> (item ?p ?plist) (sentence ?p))`

` (= ?x (cons 'or ?plist)))))`

`(defrelation implication (?x) :=`

` (exists (?plist)`

` (and (list ?plist)`

` (>= (length ?plist) 2)`

` (=> (item ?p ?plist) (sentence ?p))`

` (= ?x (cons '=> ?plist)))))`

`(defrelation reverse-implication (?x) :=`

` (exists (?plist)`

` (and (list ?plist)`

` (>= (length ?plist) 2)`

` (=> (item ?p ?plist) (sentence ?p))`

` (= ?x (cons '<= ?plist)))))`

`(defrelation equivalence (?x) :=`

` (exists (?p1 ?p2)`

` (and (sentence ?p1)`

` (sentence ?p2)`

` (= ?x `(<=> ,?p1 ,?p2)))))`

`(defrelation quantsent (?x) :=`

` (or (exists (?v ?p)`

` (and (indvar ?v) (sentence ?p)`

` (or (= ?x (listof 'forall ?v ?p))`

` (= ?x (listof 'exists ?v ?p)))))`

` (exists (?vlist ?p)`

` (and (list ?vlist) (sentence ?p)`

` (>= (length ?vlist) 1)`

` (=> (item ?v ?vlist) (indvar ?v))`

` (or (= ?x (listof 'forall ?vlist ?p))`

` (= ?x (listof 'exists ?vlist ?p)))))))`

Wed Dec 7 13:23:42 PST 1994