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