Table of Contents

Function Define-Axiom

(define-axiom <axiom-name>
       [<docstring>]
       := <sentence>
       [:theory <theory-name>]
       [:implementation <target-system-name>]
       [:issues <issue-tree>])

Macro for asserting an arbitrary OntoLingua axiom. No arguments are evaluated. See also CREATE-AXIOM, which is the functional form. Most axioms can be associated with a definition, and belong there. Some axioms involve several basic terms and are central to the theory being specified by the ontology. Such axioms are given with this form.

<axiom-name> should be a symbol which names the axiom being defined.

<docstring> The value of this keyword argument should be a string which describes the axiom being defined. It will be stored as the Lisp documentation (of type OL:ONTO-AXIOM) for the symbol which names the axiom.

The remaining keyword arguments may occur in any order, and are described below:

:= - The value of this keyword argument should be a KIF sentence which embodies the axiom to be defined.

:IMPLEMENTATION - The value of this keyword argument should be a symbol (usually a keyword) which names the target representation system in which the definition should be defined. This is independent of the theory in which the defined is defined. If the :IMPLEMENTATION argument is not supplied, the current implementation is assumed (see IN-IMPLEMENTATION.)

:ISSUES - The value of this argument should be a Lisp "tree" of strings. The tree can be either a string, or a list of strings, or a list of (<label> <any-lisp-object>) pairs, where <label> is a string or symbol that names the type of the comment. For examples,

   :issues ("This is a footnote about FOO."
            (:example (= (foo ?x) (inverse (bar ?x))))
            ("Why not do it this way?

:THEORY - The value of this keyword argument should be a symbol which names the theory in which the definition should be defined. If the :THEORY argument is not supplied, the current theory is assumed (see IN-THEORY.)