<!-- ckml.dtd
  Built from Washington State U. grammar specifying what ckml looks like.
  Public identifier is ???  -//HRL//DTD CKML 0.1//EN
  Includes oml.dtd functionality.  For OML only, use Ontology element.
-->

<!ENTITY % URI   "CDATA">  <!-- URI-reference, interpreted per [URI] -->

<!ENTITY % date  "CDATA">  <!-- any legal CKML Date instance -->

<!ENTITY % agent "CDATA">  <!-- any legal CKML Agent instance -->

<!ENTITY % typeNSname "NMTOKEN"> <!-- Format: [ name ':' ] name -->

<!ENTITY % instanceNSname "NMTOKEN"> <!-- Format: [ name '#' ] name -->

<!ENTITY % idObjAttr "id ID #IMPLIED
                      obj %instanceNSname; #IMPLIED">

<!ENTITY % fnTail "Function">  <!-- Function with type info only -->

<!ENTITY % functionLambda "Function">  <!-- Function with expr -->

<!ENTITY % objectAtomic "Object">  <!-- Restricted to atomic case -->
<!ENTITY % displayAttr  "text    CDATA #IMPLIED
			 picture %URI; #IMPLIED
			 sound   %URI; #IMPLIED">

<!ENTITY % dateAttr     "date.created %date; #IMPLIED">

<!ENTITY % creatorAttr  "creator %agent; #IMPLIED">

<!ENTITY % prefixAttr   "prefix NMTOKEN "> <!-- prefix part of namespace name 'prefix:type#id' -->

<!ENTITY % declTypeAttr "type NMTOKEN #REQUIRED"> <!-- type part of namespace name -->

<!ENTITY % shortAttr    "short NMTOKEN #IMPLIED"> <!-- short form of either type or id part of namespace name -->

<!ENTITY % referencedTypeAttr "type %typeNSname; #REQUIRED"> <!-- in collection, functionLambda, exists, forall -->

<!ENTITY % varAttr      "var NMTOKEN #REQUIRED">

<!ENTITY % genusAttr    "genus %typeNSname">  <!-- in theory -->

<!ENTITY % firstAttr    "first %typeNSname; #REQUIRED">

<!ENTITY % secondAttr   "second %typeNSname; #REQUIRED">

<!ENTITY % theoryAttr   "theory %typeNSname; "> <!-- in localLogic -->

<!ENTITY % ontologyTheoryAttr "%ontology %URI; #IMPLIED
				 %theoryAttr; #IMPLIED "> <!-- need one -->

<!ENTITY % interpretationAttr "interpretation %typeNSname;"> <!-- in localLogic -->

<!ENTITY % number "CDATA"> <!-- any legal XML number symbol-->

<!ENTITY % argcntAttr   "argcnt %number; #IMPLIED">

<!ENTITY % aboutAttr    "about %URI; #IMPLIED">

<!ENTITY % srcTypeAttr  "srcType %typeNSname; #REQUIRED">  <!-- in function, argument -->

<!ENTITY % tgtTypeAttr  "tgtType %typeNSname; #REQUIRED">  <!-- in function, argument -->

<!ENTITY % srctgtTypeAttr "srcType %typeNSname; #IMPLIED"  <!-- one required -->
			  "tgtType %typeNSname; #REQUIRED">

<!ENTITY % order	"(less|lessEqual|equal|greater|greaterEqual)">

<!ENTITY % ordAttr      "order %order; #IMPLIED">




<!-- Top level element             CKML


-->
<!ELEMENT CKML (Ontology | %typeNSname;) >

<!ENTITY % specification "Assertion | Object | Relation | BinaryRelation | Function
			| Collection | constant | Product | Sum | Theory
			| interpretation">

<!ENTITY % axiom "sequent | synonymous | subtype | disjoint | partition 
		| transpose | inverse">



<!-- Top level element             Ontology


-->
<!ELEMENT Ontology (comment?, (extends | %specification; | %axiom;)*) >
<!ATTLIST Ontology id ID #REQUIRED
		   %displayAttr;
		   %dateAttr;
		   %creatorAttr;
		   version CDATA #REQUIRED
		   %prefixAttr; #IMPLIED >

<!ELEMENT extends EMPTY >
<!ATTLIST extends %ontologyTheoryAttr; 
		  %prefixAttr; #REQUIRED >

<!ELEMENT Assertion ANY > <!-- really (comment?, expr) -->
<!ATTLIST Assertion id ID #IMPLIED
		    text CDATA #IMPLIED>

<!-- Note that not all objects reasonably usable in every context -->
<!ELEMENT Object ANY> <!-- Really (comment?, (%fnTail;* | expr)) for (Atomic | other) -->
<!ATTLIST Object %declTypeAttr; 
		 %shortAttr;
		 %dateAttr;
		 %creatorAttr;
		 %referencedTypeAttr;  <!-- Interpreted only -->
		 %varAttr; <!-- Not on Atomic -->
		 %genusAttr; #REQUIRED > <!-- Not on Atomic -->

<!ELEMENT Product EMPTY >  <!-- objects -->
<!ATTLIST Product %declTypeAttr; 
		  %firstAttr;
		  %secondAttr; >

<!ELEMENT Sum EMPTY >  <!-- objects -->
<!ATTLIST Sum %declTypeAttr; 
	      %firstAttr;
	      %secondAttr;>

<!ELEMENT Relation (comment?, (%fnTail;* | %functionLambda;*)) >  <!-- (Atomic | Defined) -->
<!ATTLIST Relation %declTypeAttr; 
		   %shortAttr;
		   %dateAttr;
		   %creatorAttr; >

<!ELEMENT Collection ANY> <!-- Really (comment?, expr?),  need contents for Defined case -->
<!ATTLIST Collection type NMTOKEN #IMPLIED  <!-- Need for Atomic case -->
		     %varAttr;  <!-- need for Defined case -->
		     %genusAttr; #IMPLIED >

<!ELEMENT BinaryRelation (comment)? >
<!ATTLIST BinaryRelation %declTypeAttr; 
			 %srcTypeAttr;
			 %tgtTypeAttr; >

<!-- not every kind of Function usable everywhere.  No body for Atomic or Tail,
  collection or relation for Defined, fnLambda or expr for Lambda
 -->
<!ELEMENT Function ANY> <!-- Really (comment?, (Collection | Relation | %functionLambda; | expr)?) -->
<!ATTLIST Function %declTypeAttr; 
		   %varAttr;  <!-- Defined or Lambda case only -->
		   %srctgtTypeAttr; > <!-- need both if atomic, src if Defined,
		   			  tgt if Lambda, either if Tail -->


<!ELEMENT Theory (comment?, (extends*, %objectAtomic;*,
                    (sequent | synonymous | subtype | disjoint | partition)* ,
                    Interpretation*, Theory*)?) > <!-- EMPTY if embedded -->
<!ATTLIST Theory %declTypeAttr; 
		 ontology %URI; #IMPLIED  <!-- embedded ontology only -->
		 %genusAttr; #IMPLIED >

<!ELEMENT Interpretation (comment?, (objectInterpreted)*) >
<!ATTLIST Interpretation %declTypeAttr; 
			 fnType %typeNSname; #REQUIRED >

<!-- No elements currently refer to LocalLogic! -->
<!ELEMENT LocalLogic (comment?, (Argument)*)> <*-- EMPTY except relType case -->
<!ATTLIST LocalLogic %declTypeAttr;
		     <!-- At least one of the following must occur -->
		     %theoryAttr; #IMPLIED  <!-- given theory -->
                     binrelType %typeNSname; #IMPLIED <!-- direct scaling, option on theory -->
                     %interpretationAttr; #IMPLIED <!-- simple scaling -->
                     relType %typeNSname; #IMPLIED> <!-- relational scaling -->
                             (comment? Argument*)

<!ELEMENT Argument (Interpretation)? >  <!-- Attr or Arg but not both -->
<!ATTLIST Argument %referencedTypeAttr; 
		   %interpretationAttr; #IMPLIED >

<!ELEMENT Interpretation EMPTY >
<!ATTLIST Interpretation %referencedTypeAttr; >

<!ELEMENT sequent ANY >  <!-- Really one or more user defined instances -->

<!ELEMENT synonymous (comment)? >
<!ATTLIST synonymous %firstAttr; %secondAttr; >

<!ELEMENT subtype (comment)? >
<!ATTLIST subtype specific %typeNSname; #REQUIRED
        	  generic  %typeNSname; #IMPLIED >

<!ELEMENT disjoint ANY >  <!-- Really one or more user defined instances -->

<!ELEMENT partition ANY >  <!-- Really one or more user defined instances -->

<!ELEMENT transpose (comment)? >
<!ATTLIST transpose %firstAttr; 
		    %secondAttr; > <!-- Binary relations -->

<!ELEMENT inverse (comment)? >
<!ATTLIST inverse %firstAttr;
		  %secondAttr; > <!-- functions        -->

<!-- Format of typical user written collection Instance 
  <!ELEMENT %typeNSname; ANY > <!-- Really one or more user defined instances -->
  <!ATTLIST %typeNSname; id ID #IMPLIED 
			 ontology %UID; #IMPLIED > 
-->

<!-- Format of typical user written localLogic Instance --
  <!ELEMENT %typeNSname; ANY > <!-- Really (objectInstance | typ)* -->
  <!ATTLIST %typeNSname; id ID #REQUIRED >
-->

<!ELEMENT typ ANY>  <!-- Really any user written type name -->
<!ATTLIST typ obj = %instanceNSname; #REQUIRED >

<!-- Format of user-written type name 
  <!ELEMENT %typeNSname; EMPTY >  
-->

<!-- Format of typical user written object Instance  --
  <!ELEMENT %typeNSname; (fnInstTail)*>
  <!ATTLIST %typeNSname; %idObjAttr;
			 %shortAttr;
			 %aboutAttr;  <!-- One of about, display or description -->
			 %displayAttr;
			 description %instanceNSname; #IMPLIED >
-->

<!-- Format of typical user written relation Instance --
  <!ELEMENT %typeNSname; (comment?, (fnInstTail)*)>
  <!ATTLIST %typeNSname; %idObjAttr; 
			 %shortAttr;
			 binrel %typeNSname; #REQUIRED >
-->

<!-- Format of typical user written binrel Instance --
  <!ELEMENT %typeNSname; (comment)? >
  <!ATTLIST %typeNSname; src %instanceNSname; #REQUIRED
              		 tgt %instanceNSname; #REQUIRED >
-->

<!-- Format of typical user written function Instance --
  <!ELEMENT %typeNSname; (comment)? >
  <!ATTLIST %typeNSname; %ordAttr;
              		 src %instanceNSname; #REQUIRED
              		 tgt %instanceNSname; #REQUIRED > 
-->

<!-- Format of typical user written fnInstTail
  <!ELEMENT %typeNSname; ANY > <!-- Really (#PCDATA | objectInstance) -->
  <!ATTLIST %typeNSname; %ordAttr;
              		 src %instanceNSname; #REQUIRED <!-- src,tgt in place of body -->
              		 tgt %instanceNSname; #REQUIRED > 
-->

<!ELEMENT comment (#PCDATA)>

<!-- Because of the instances, forces ANY where used.
<!ENTITY % expr  "relationInstance | binrelInstance | functionInstance
                       | and | or | not | implies | equiv | exists | forall">
-->

<!ELEMENT and ANY> <!-- really (comment?, expr*) -->
<!ATTLIST and %argcntAttr;>

<!ELEMENT or ANY> <!-- really (comment?, expr*) -->
<!ATTLIST or %argcntAttr;>

<!ELEMENT not ANY> <!-- really (comment?, expr*) -->

<!ELEMENT implies ANY> <!-- really (comment?, expr, expr) -->

<!ELEMENT equiv ANY> <!-- really (comment?, expr, expr) -->

<!ELEMENT Exists ANY> <!-- really (comment?, expr) -->
<!ATTLIST Exists %varAttr; 
		 %referencedTypeAttr; >

<!ELEMENT Forall ANY> <!-- really (comment?, expr) -->
<!ATTLIST Forall %varAttr; 
		 %referencedTypeAttr; >