Formalizing Syntax



next up previous
Next: Changing Levels of Up: Metaknowledge Previous: Naming Expressions

Formalizing Syntax

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



Vishal I. Sikka
Wed Dec 7 13:23:42 PST 1994