(in-package "ONTOLINGUA-USER")
(define-ontology KIF-META (kif-sets kif-lists)
"The KIF vocabulary for representing metalinguistic knowledge."
:maturity :very-high
:generality :very-high
:issues ("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-ontology 'kif-meta)
(define-class EXPRESSION (?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-class WORD (?expr)
"An atom in a KIF expression."
:def (and (expression ?expr)
(not (list ?expr)))
:axiom-def (exhaustive-subclass-partition@frame-ontology
WORD (setof variable
constant))
:issues (("Word used to be partitioned into variable, constant, and OPERATOR,
but examination of p.8 of the spec reveals that operators are not
words, which is a relief because this was causing exhaustive-
subclass partition barfage because variable and constant were
both members of the partitions of Word and Term. Term has been
updated so as to be partitioned into Word and the non-atomic
terms. JPR.")))
(define-class VARIABLE (?expr)
"KIF variable"
:def (word ?expr)
:axiom-def (exhaustive-subclass-partition@frame-ontology
VARIABLE (setof indvar seqvar)))
(define-class OPERATOR (?expr)
"KIF operator"
:def (not (list ?expr))
:axiom-def (exhaustive-subclass-partition@frame-ontology OPERATOR
(setof termop sentop ruleop defop)))
(define-class CONSTANT (?expr)
"A constant used in a KIF expression."
:def (word ?expr)
:axiom-def (exhaustive-subclass-partition@frame-ontology CONSTANT
(setof funconst relconst objconst)))
(define-class FUNCONST (?symbol)
"A symbol that denotes a function. Used as the functor of a
term expression."
:def (constant ?symbol))
(define-class RELCONST (?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-class OBJCONST (?symbol)
"A symbol that denotes a KIF object other than a relation."
:def (constant ?symbol))
(define-class INDVAR (?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-class SEQVAR (?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-class TERMOP (?expr)
"KIF term operator"
:iff-def (member ?expr
(setof 'quote 'listof 'cond 'the 'setof
'setofall 'kappa 'lambda))
:constraints (operator ?expr))
(define-class SENTOP (?expr)
"KIF sentence operator"
:iff-def (member ?expr
(setof 'not 'and 'or
'=> '<= '<=>
'forall 'exists))
:constraints (operator ?expr))
(define-class RULEOP (?expr)
"KIF rule operator"
:iff-def (member ?expr
(setof '=>> '<<=))
:constraints (operator ?expr))
(define-class DEFOP (?expr)
"KIF definitional operator"
:iff-def (member ?expr
(setof 'defobject 'define-function 'defrelation
':= ':=> ':axiom
':conservative-axiom))
:constraints (operator ?expr))
(define-class TERM (?expr)
"KIF term expression"
:iff-def (expression ?expr)
:axiom-def (exhaustive-subclass-partition@frame-ontology TERM
(setof ;;variable constant ;; atomic terms - used to be these.
word
funterm listterm setterm
quoterm logterm quanterm))
:issues (("See notes on Word.")))
(define-class FUNTERM (?expr)
"KIF function term expression."
:iff-def (and (term ?expr)
(list ?expr)
(funconst (first ?expr))))
(define-class LISTTERM (?expr)
"KIF list term expression"
:iff-def (and (term ?expr)
(list ?expr)
(= (first ?expr) 'listof)))
(define-class SETTERM (?expr)
"KIF set term expression"
:iff-def (and (term ?expr)
(list ?expr)
(= (first ?expr) 'setof)))
(define-class QUOTERM (?expr)
"KIF quoted term expression."
:iff-def (and (term ?expr)
(list ?expr)
(= (first ?expr) 'quote)
(expression (first (first ?expr)))))
(define-class LOGTERM (?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-class QUANTERM (?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-class SENTENCE (?expr)
"KIF sentence expression. Has a truth value."
:def (expression ?expr)
:axiom-def (exhaustive-subclass-partition@frame-ontology SENTENCE
(setof logconst relsent logsent quantsent)))
(define-class LOGCONST (?x)
"A KIF logical constant."
:def (sentence ?x))
(define-class RELSENT (?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-class EQUATION (?x)
:iff-def (and (relsent ?x)
(exists (?t1 ?t2)
(and (term ?t1) (term ?t2)
(= ?x (listof '= ?t1 ?t2))))))
(define-class INEQUALITY (?x)
:iff-def (and (relsent ?x)
(exists (?t1 ?t2)
(and (term ?t1) (term ?t2)
(= ?x (listof '/= ?t1 ?t2))))))
(define-class LOGSENT (?expr)
"KIF logical sentence."
:def (sentence ?expr)
:axiom-def (exhaustive-subclass-partition@frame-ontology LOGSENT
(setof negation conjunction disjunction
implication reverse-implication equivalence)))
(define-class NEGATION (?x)
:iff-def (exists (?p)
(and (sentence ?p)
(= ?x (listof 'NOT ?p))))
:constraints (logsent ?x))
(define-class CONJUNCTION (?x)
:iff-def (exists ?plist
(and (list ?plist)
(>= (length ?plist) 1)
(=> (item ?p ?plist) (sentence ?p))
(= ?x (cons 'AND ?plist))))
:constraints (logsent ?x))
(define-class DISJUNCTION (?x)
:iff-def (exists ?plist
(and (list ?plist)
(>= (length ?plist) 1)
(=> (item ?p ?plist) (sentence ?p))
(= ?x (cons 'or ?plist))))
:constraints (logsent ?x))
(define-class IMPLICATION (?x)
:iff-def (exists (?plist)
(and (list ?plist)
(>= (length ?plist) 2)
(=> (item ?p ?plist) (sentence ?p))
(= ?x (cons '=> ?plist))))
:constraints (logsent ?x))
(define-class REVERSE-IMPLICATION (?x)
:iff-def (exists (?plist)
(and (list ?plist)
(>= (length ?plist) 2)
(=> (item ?p ?plist) (sentence ?p))
(= ?x (cons '<= ?plist))))
:constraints (logsent ?x))
(define-class EQUIVALENCE (?x)
:iff-def (exists (?p1 ?p2)
(and (sentence ?p1)
(sentence ?p2)
(= ?x (listof '<=> ?p1 ?p2))))
:constraints (logsent ?x))
(define-class QUANTSENT (?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-function DENOTATION (?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-function NAME (?x) :-> ?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.)")
(define-relation TRUTH (?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-relation DEFINING-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-relation ANALYTIC-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))