BNF for Ontolingua

• Mail folder: Ontolingua Mail
• Next message: Tom Gruber: "example ontology for bibliographies"
• Previous message: Tom Gruber: "what's new in ontolingua 3?"

Message-id: <2922681001-6756346@KSL-Mac-69>
Date: Thu, 13 Aug 92  00:50:01 PDT
From: Tom Gruber <Gruber@Sumex-AIM.Stanford.edu>
To: ontolingua@SUMEX-AIM.Stanford.EDU
Subject: BNF for Ontolingua

Here is a BNF description of the new syntax for Ontolingua.
The official version is maintained in the reference manual.
Please send reports of errors to the list.

<definition> :== <relation-def> | <class-def> | <function-def> |
                 <instance-def> | <axiom-def> | <theory-def>

<relation-def> :== (DEFINE-RELATION <relation-name> (<var> [<var>]*)
                      [<docstring>]
                      {:def | :iff-def} <sent-with-arg-vars>
                      [:constraints <sent-with-arg-vars>]
                      [:equivalent <sent-with-arg-vars>]
                      [:sufficient <sent-with-arg-vars>]
                      [:default-constraints <sent-with-arg-vars>]
                      [:axiom-def <sent-without-arg-vars>]
                      [:axiom-constraints <sent-without-arg-vars>]
                      [:theory <theory-name>]
                      [:issues <issue-tree>])

<class-def> :== (DEFINE-CLASS <class-name> (<var>)
                      [<docstring>]
                      {:def | :iff-def} <sent-with-arg-vars>
                      [:constraints <sent-with-arg-vars>]
                      [:equivalent <sent-with-arg-vars>]
                      [:sufficient <sent-with-arg-vars>]
                      [:default-constraints <sent-with-arg-vars>]
                      [:axiom-def <sent-without-arg-vars>]
                      [:axiom-constraints <sent-without-arg-vars>]
                      [:theory <theory-name>]
                      [:issues <issue-tree>])

<function-def> :== (DEFINE-FUNCTION <function-name> (<var> [<var>]*) [:-> <var>]
                      [<docstring>]
                      [{:def | :iff-def} <sent-with-arg-vars>]
                      [:constraints <sent-with-arg-vars>]
                      [:axiom-def <sent-without-arg-vars>]
                      [:axiom-constraints <sent-without-arg-vars>]
                      [:lambda-body <term-expression-with-arg-vars>]
                      [:theory <theory-name>]
                      [:issues <issue-tree>])

<instance-def> :== (DEFINE-INSTANCE <instance-name> (<class-name> [<class-name>]*)
                      [<docstring>]
                      {{:= <term-expression-without-arg-vars>} |
                       {:axiom-def <sent-without-arg-vars>}}
                      [:theory <theory-name>]
                      [:issues <issue-tree>])

<axiom-def> :== (DEFINE-AXIOM <axiom-name>
                      [<docstring>]
                      := <sentence>
                      [:theory <theory-name>]
                      [:issues <issue-tree>])

<theory-def> :== (DEFINE-THEORY <theory-name> ([<theory-name>]*)
                      [<docstring>]
                      [:implementation <target-KR-system-name>]
                      [:io-package <Lisp package name>]
                      [:issues <issue-tree>])

<issue-tree> :== ({<string> | <symbol> | <issue-tree>}+)
<docstring> :== <string>
<issue-string> :== <string>
<string>  :== string enclosed in "double quotes", and used as
<var> :== symbol beginning with '?'
<name> :== symbol not beginning with '?','@', or '$' 
           and used as exactly one of:
  <relation-name> :== <name>
  <class-name> :== <name>
  <function-name> :== <name>
  <instance-name> :== <name>
  <axiom-name> :== <name>
  <theory-name> :== <name>
<sent-with-arg-vars> :== KIF sentence mentioning at least one of the vars in
                         the argument list to the definition
<sent-without-arg-vars> :== KIF sentence mentioning the name of the thing
                            being defined but not the argument vars
<term-expression-with-arg-vars> :== KIF term expression mentioning all of the 
                                    argument variables (but not the value var)
<term-expression-without-arg-vars> :== KIF term expression mentioning the 
                                       function being defined
<sentence> :== any old KIF sentence