;;; -*- 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-theory KIF-META (kif-sets kif-lists)
  "The KIF vocabulary for representing metalinguistic knowledge.")


(in-theory '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
               WORD (setof variable operator constant)))

(define-class VARIABLE (?expr)
  "KIF variable"
  :def (and (word ?expr)
	    (term ?expr))
  :axiom-def (exhaustive-subclass-partition
               VARIABLE (setof indvar seqvar)))

(define-class OPERATOR (?expr)
  "KIF operator"
  :def (and (word ?expr)
	    (term ?expr))
  :axiom-def (exhaustive-subclass-partition OPERATOR
             (setof termop sentop ruleop defop)))

(define-class CONSTANT (?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-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 TERM
              (setof variable constant listterm setterm
                     quoterm logterm quanterm)))

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