An XML DTD for CL

<!-- A DTD for XML instantiations of the Common Logic language -->

<!--"theory" is taken as the root element, as the DTD can then be applied to 
sets of formulas.-->

<!ELEMENT theory (formula*)>

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

<!ELEMENT and (formula*)>

<!ELEMENT or (formula*)>

<!ELEMENT implies (formula)>

<!ELEMENT iff (formula)>

<!ELEMENT not (formula)>

<!ELEMENT forall (varlist, formula)>

<!ELEMENT exists (varlist, varlist*, formula)>

<!ELEMENT atom ((con | var | fnterm), (con | var | fnterm | seqvar)*)>

<!ELEMENT fnterm ((con | var | fnterm), (con | var | fnterm | seqvar)*)>

<!ELEMENT varlist (var | seqvar | sortvar)*>

<!ELEMENT sortvar (var, con)>

<!ELEMENT con (#PCDATA)>

<!ELEMENT var (#PCDATA)>

<!ELEMENT seqvar (#PCDATA)>