<!-- An XML DTD for a Hornfun RuleML Sublanguage -->
<!-- Last Modification: 2002-07-09 -->


<!-- ENTITY Declarations -->


<!ENTITY % rellog.module "IGNORE">
<!ENTITY % datalog.module "IGNORE">
<!ENTITY % datalog-and-hornlog.module "INCLUDE">
<!ENTITY % datafun.module "IGNORE">

<!ENTITY % datafun SYSTEM "ruleml-datafun.dtd">
%datafun;


<!-- Start region that should be imported from a version of ruleml-hornlog.dtd -->

<!-- ELEMENT Declarations -->


<!-- complex, compound, or constructor terms are usable within other cterms, tups, rolis, and atoms -->
<!-- cterm element uses _opc ("operator of constructors") role followed by sequence of five kinds of arguments, -->
<!-- or vice versa, much like atoms (explained below) -->
 
<!ELEMENT cterm ((_opc, (ind | var | cterm | tup | roli)*) | ((ind | var | cterm | tup | roli)+, _opc))>


<!-- _opc is usable within c(onstructor )terms -->
<!-- _opc uses c(onstruc)tor symbol -->

<!ELEMENT _opc (ctor)>


<!-- constructors -->
<!ELEMENT ctor (#PCDATA)>


<!-- NOTICE: tups and rolis are still very preliminary -->

<!-- n-tuples are usable within other tups, rolis, cterms, and atoms -->
<!-- tup element uses sequence of five kinds of arguments -->

<!ELEMENT tup   ((ind | var | cterm | tup | roli)*)>


<!-- "roli" is short for "role list" -->
<!-- sequence is not (syntactically) significant among its children, i.e., it is sequence-free -->

<!ELEMENT roli ((_arv)*)>
<!ELEMENT _arv ((arole, (ind | var | cterm | tup | roli)) | ((ind | var | cterm | tup | roli), arole)) >
<!ELEMENT arole (#PCDATA)>


<!-- "_rbaselab" is is short for "rulebase label"; may be ind(ividual) or c(onstructor )term;
     this allows naming of an entire individual rulebase in a fashion that is accessible
     within the knowledge representation; -->
<!-- e.g., this can help for representing prioritization between rulebases, or perhaps
     to enable forward inferencing of selected rulebase(s)  -->

<!-- SYNTACTIC REQUIREMENT BEYOND DTD:  for now, must be GROUND (e.g., if cterm) -->

<!-- FUTURE DESIGN:  might permit to be non-ground;
     e.g., to instantiate a personal messaging agent to the particular user; 
     but that would require that coincidence of variable names be significant ACROSS rules,
     and there are expressively simpler ways to achieve the same effect -->

<!ELEMENT _rbaselab (ind | cterm)>


<!-- "_rlab" is short for "rule label"; may be ind(ividual) or c(onstructor )term;
     this allows naming of a rule (either imp or fact) in a fashion that is accessible
     within the knowledge representation; -->
<!-- e.g., this can help for representing prioritization between rules -->

<!-- NOTE:  rule labels are not required to be unique within a rulebase -->

<!-- SYNTACTIC REQUIREMENT BEYOND DTD:  any logical variables (var elements)
appearing within the rule label (i.e., within _rlab's cterm child) must also appear within
the rule body and/or head --> 
<!-- FUTURE DESIGN:  probably will want to permit even stronger restrictions on the
appearance of variables, e.g., 
"must appear within both the rule head and body" or
"must appear within the rule body but not in any literal which has negation-as-failure,
nor in any literal which can sensed" in OLP or CLP or SLP or SCLP -->

<!-- NOTE:  rule label is not required to be ground; semantically, instantiating
the rule label's logical variables corresponds to instantiating the (rest of the)
rule's variables.  For example, if the rule says "Mortal(?x) if Man(?x)", and
the rule label is "SocraticSyllogism(?x)", then "SocraticSyllogism(Joe)" 
corresponds semantically to the rule label for "Mortal(Joe) if Man(Joe)".  
 -->
  
<!ELEMENT _rlab (ind | cterm) >


<!-- atomic formulas are usable within _head's, _body's, 'and's, and 'andv's -->
<!-- atom element uses an: -->
<!-- _opr ("operator of relations") role followed by a sequence of zero or more arguments, or similarly -->
<!-- (since roles constitute unordered elements, and the zero-argument case must not cause ambiguity), -->
<!-- a sequence of one or more arguments followed by an _opr role -->
<!-- the arguments may be ind(ividual)s, var(iable)s, c(onstructor )terms, (n-)tup(le)s, or ro(le )li(st)s -->

<!ELEMENT atom ((_opr, (ind | var | cterm | tup | roli)*) | ((ind | var | cterm | tup | roli)+, _opr))>

<!-- End region that should be imported from a version of ruleml-hornlog.dtd -->


<!-- _foot role is usable within 'trans' rules -->
<!-- _foot uses an ind, var, a nano formula, a nano 'by-value' formula, or a cterm, tup, or roli  -->

<!ELEMENT _foot (ind | var | nano | nanov | cterm | tup | roli)>


<!-- atomic 'by-value' formulas are usable within _body's, and 'andv's -->
<!-- atomv element uses _opr ("operator of relations") role followed by seven kinds of arguments, -->
<!-- or vice versa, extending atoms -->

<!ELEMENT atomv ((_opr, (ind | var | nano | nanov | cterm | tup | roli)*) | ((ind | var | nano | nanov | cterm | tup | roli)+, _opr))>


<!-- nano formulas are usable within _headf's, _foot's, atomv's, and nanov's -->
<!-- nano element uses _opf ("operator of functions") role followed by five kinds of arguments, -->
<!-- or vice versa, much like atoms  -->

<!ELEMENT nano ((_opf, (ind | var | cterm | tup | roli)*) | ((ind | var | cterm | tup | roli)+, _opf))>

<!-- nanov formulas are usable within _foot's, atomv's, and nanov's -->
<!-- nanov element uses _opf ("operator of functions") role followed by seven kinds of arguments -->
<!-- or vice versa, extending nanos -->

<!ELEMENT nanov ((_opf, (ind | var | nano | nanov | cterm | tup | roli)*) | ((ind | var | nano | nanov | cterm | tup | roli)+, _opf))>