[SCL] DTD for XML/SCL

[Chris Menzel]

On Sun, Dec 22, 2002 at 06:49:26PM -0500, Bill Andersen wrote:
> ...
> I personally like something like this (#2), except with a modification 
> to make the predicate and function terms themselves analogs to the 
> existing abstract syntax.  See below.
> ... 
> <implies>
>   <forall>
>     <varlist>
>       <var>x</var>
>     </varlist>
>     <atomic>
>       <term>P</term>
>       <fnterm>
>         <term>succ</term>
>         <term>x</term>
>       </fnterm>
>     </atomic>
>   </forall>
>   <atomic>
>     <term>P</term>
>     <fnterm>
>       <term>succ</term>
>       <term>0</term>
>     </fnterm>
>   </atomic>
> </implies>

I agree that this is the right approach if we want to remain consistent
with the current CL approach.  Here's a simple DTD that seems to do the
job.  It is a bit more fine-grained than Bill suggests, as it retains
the distinction between constants and variables (following CL).
Restricted quantifiers are allowed (via the "sortvar" element), also in
accordance with CL and an earlier suggestion of Tanel's.  I suggest
taking "theory" to be the root element, so that the DTD will apply to
sets of formulas, notably, the formulas constituting an ontology.
Constants and variables are just taken to be unspecified PCDATA in the
DTD, but could be added explicitly if a fixed lexicon is desired (though
I'm not exactly sure how to do that in a DTD if one wants infinitely
many variables).

<!ELEMENT theory (formula*)>

<!ELEMENT formula (and | or | implies | iff | not | forall | exists | atomic)>

<!ELEMENT and (formula*)>

<!ELEMENT or (formula*)>

<!ELEMENT implies (formula, formula)>

<!ELEMENT iff (formula, formula)>

<!ELEMENT not (formula)>

<!ELEMENT forall (varlist, formula)>

<!ELEMENT exists (varlist, formula)>

<!ELEMENT atomic (con | var | fnterm)+>

<!ELEMENT fnterm (con | var | fnterm), (con | var | fnterm)+>

<!ELEMENT varlist (var | sortvar)*>

<!ELEMENT sortvar (var, con)>

<!ELEMENT con (#PCDATA)>

<!ELEMENT var (#PCDATA)>

I've added a slightly more general DTD for full CL to the current CL doc
(not yet online).  Comments encouraged.

-chris