;;; -*- Mode:Lisp; Syntax:Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-;;; If you load this file (with translation into the "KIF" implementation;;; -- the default ), then the definitions are saved on property lists;;; and can be used for online documentation and in cross-reference reports.(in-package "ONTOLINGUA-USER") ;inherits from the KIF package;all constants defined here are exported;from the KIF package.(define-theoryKIF-META(kif-sets kif-lists) "The KIF vocabulary for representing metalinguistic knowledge.") (in-theory 'kif-meta) (define-classEXPRESSION(?expr) "KIF expression is either a word or a list of expressions." :iff-def (or (word ?expr) (and (list ?expr) (forall ?subexpr (=> (item ?subexpr ?expr) (expression ?subexpr)))))) (define-classWORD(?expr) "An atom in a KIF expression." :def (and (expression ?expr) (not (list ?expr))) :axiom-def (exhaustive-subclass-partition WORD (setof variable operator constant))) (define-classVARIABLE(?expr) "KIF variable" :def (and (word ?expr) (term ?expr)) :axiom-def (exhaustive-subclass-partition VARIABLE (setof indvar seqvar))) (define-classOPERATOR(?expr) "KIF operator" :def (and (word ?expr) (term ?expr)) :axiom-def (exhaustive-subclass-partition OPERATOR (setof termop sentop ruleop defop))) (define-classCONSTANT(?expr) "A constant used in a KIF expression." :def (and (word ?expr) (term ?expr)) :axiom-def (exhaustive-subclass-partition CONSTANT (setof funconst relconst objconst))) (define-classFUNCONST(?symbol) "A symbol that denotes a function. Used as the functor of a term expression." :def (constant ?symbol)) (define-classRELCONST(?symbol) "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." :def (constant ?symbol)) (define-classOBJCONST(?symbol) "A symbol that denotes a KIF object other than a relation." :def (constant ?symbol)) (define-classINDVAR(?expression) "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." :def (variable ?expression)) (define-classSEQVAR(?expression) "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." :def (variable ?expression)) (define-classTERMOP(?expr) "KIF term operator" :iff-def (member ?expr (setof 'quote 'listof 'cond 'the 'setof 'setofall 'kappa 'lambda)) :constraints (operator ?expr)) (define-classSENTOP(?expr) "KIF sentence operator" :iff-def (member ?expr (setof 'not 'and 'or '=> '<='<=>'forall 'exists)) :constraints (operator ?expr)) (define-classRULEOP(?expr) "KIF rule operator" :iff-def (member ?expr (setof '=>> '<<=)) :constraints (operator ?expr)) (define-classDEFOP(?expr) "KIF definitional operator" :iff-def (member ?expr (setof 'defobject 'define-function 'defrelation ':= ':=> ':axiom ':conservative-axiom)) :constraints (operator ?expr)) (define-classTERM(?expr) "KIF term expression" :iff-def (expression ?expr) :axiom-def (exhaustive-subclass-partition TERM (setof variable constant listterm setterm quoterm logterm quanterm))) (define-classFUNTERM(?expr) "KIF function term expression." :iff-def (and (term ?expr) (list ?expr) (funconst (first ?expr)))) (define-classLISTTERM(?expr) "KIF list term expression" :iff-def (and (term ?expr) (list ?expr) (= (first ?expr) 'listof))) (define-classSETTERM(?expr) "KIF set term expression" :iff-def (and (term ?expr) (list ?expr) (= (first ?expr) 'setof))) (define-classQUOTERM(?expr) "KIF quoted term expression." :iff-def (and (term ?expr) (list ?expr) (= (first ?expr) 'quote) (expression (first (first ?expr))))) (define-classLOGTERM(?x) :iff-def (or (exists (?p1 ?t1) (and (sentence ?p1) (term ?t1) (= ?x (listof 'IF ?p1 ?t1)))) (exists (?p1 ?t1 ?t2) (and (sentence ?p1) (term ?t1) (term ?t2) (= ?x (listof '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))))) :constraints (term ?x)) (define-classQUANTERM(?x) :iff-def (or (exists (?t ?p) (and (term ?t) (sentence ?p) (= ?x (listof 'THE ?t ?p)))) (exists (?t ?p) (and (term ?t) (sentence ?p) (= ?x (listof 'SETOFALL ?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))))) :constraints (term ?x)) (define-classSENTENCE(?expr) "KIF sentence expression. Has a truth value." :def (expression ?expr) :axiom-def (exhaustive-subclass-partition SENTENCE (setof logconst relsent logsent quantsent))) (define-classLOGCONST(?x) "A KIF logical constant." :def (sentence ?x)) (define-classRELSENT(?x) :iff-def (exists (?r ?tlist) (and (or (relconst ?r) (funconst ?r)) (list ?tlist) (>= (length ?tlist) 1) (=> (item ?t ?tlist) (term ?t)) (= ?x (cons ?r ?tlist)))) :constraints (sentence ?x)) (define-classEQUATION(?x) :iff-def (and (relsent ?x) (exists (?t1 ?t2) (and (term ?t1) (term ?t2) (= ?x (listof '= ?t1 ?t2)))))) (define-classINEQUALITY(?x) :iff-def (and (relsent ?x) (exists (?t1 ?t2) (and (term ?t1) (term ?t2) (= ?x (listof '/= ?t1 ?t2)))))) (define-classLOGSENT(?expr) "KIF logical sentence." :def (sentence ?expr) :axiom-def (exhaustive-subclass-partition LOGSENT (setof negation conjunction disjunction implication reverse-implication equivalence))) (define-classNEGATION(?x) :iff-def (exists (?p) (and (sentence ?p) (= ?x (listof 'NOT ?p)))) :constraints (logsent ?x)) (define-classCONJUNCTION(?x) :iff-def (exists ?plist (and (list ?plist) (>= (length ?plist) 1) (=> (item ?p ?plist) (sentence ?p)) (= ?x (cons 'AND ?plist)))) :constraints (logsent ?x)) (define-classDISJUNCTION(?x) :iff-def (exists ?plist (and (list ?plist) (>= (length ?plist) 1) (=> (item ?p ?plist) (sentence ?p)) (= ?x (cons 'or ?plist)))) :constraints (logsent ?x)) (define-classIMPLICATION(?x) :iff-def (exists (?plist) (and (list ?plist) (>= (length ?plist) 2) (=> (item ?p ?plist) (sentence ?p)) (= ?x (cons '=> ?plist)))) :constraints (logsent ?x)) (define-classREVERSE-IMPLICATION(?x) :iff-def (exists (?plist) (and (list ?plist) (>= (length ?plist) 2) (=> (item ?p ?plist) (sentence ?p)) (= ?x (cons '<=?plist)))) :constraints (logsent ?x)) (define-classEQUIVALENCE(?x) :iff-def (exists (?p1 ?p2) (and (sentence ?p1) (sentence ?p2) (= ?x (listof '<=>?p1 ?p2)))) :constraints (logsent ?x)) (define-classQUANTSENT(?x) :iff-def (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)))))) :constraints (sentence ?x)) (define-functionDENOTATION(?x) "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$." ) (define-functionNAME(?x) "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.)") (define-relationTRUTH(?sentence) "A level-crossing relation used to state that a sentence is true." :def (sentence ?sentence) :issues ((:example (truth '(=> (sentence ?p) (listof '=> ?p ?p)))))) (define-relationDEFINING-AXIOM(?constant ?sentence) "a defining axiom for a constant is a sentence that helps define the constant. See the KIF specification for details." :def (and (constant ?constant) (sentence ?sentence))) (define-relationANALYTIC-TRUTH(?sentence) "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$." :def (sentence ?sentence))