RIF Core Dialect

1 Overview

2 RIF-Core Presentation Syntax

Like RIF-BLD and RIF-PRD, RIF-Core has both a presentation syntax and an XML syntax. It is defined in "mathematical English," a special form of English for communicating mathematical definitions, examples, etc. and by an EBNF syntax. The mathematical English is normative, the EBNF is not normative; both instances of the presentation syntax are not intended to be a concrete syntax for RIF-Core. The English presentation syntax deliberately leaves out details such as the delimiters of the various syntactic components, escape symbols, parenthesizing, precedence of operators, and the like. Since RIF is an interchange format, it uses XML, and only XML, as its concrete syntax. RIF-Core conformance is described in terms of semantics-preserving mappings.

2.1 Alphabet of RIF-Core

2.2 Terms of RIF-Core

2.3 Formulas of RIF-Core

2.4 Annotations and Documents

RIF-Core allows every term and formula to be optionally annotated in the same way as in RIF-BLD. The frame formulas that are allowed as part of an annotation must be syntactically correct for RIF-Core. In particular, no function symbols are allowed in such a formula.

2.5 Well-formed Formulas

2.6 EBNF Grammar for the Presentation Syntax of RIF-Core

Until now, we have used mathematical English to specify the syntax of RIF-Core as a restriction on RIF-BLD. Tool developers, however, may prefer EBNF notation, which provides a more succinct view of the syntax. However, EBNF is unable to express all of the well-formedness conditions. For instance, the requirement that each symbol appear in only one context cannot be expressed in EBNF. As a result, the EBNF grammar defines a strict superset of RIF-Core. For that reason this section is not normative.

2.6.1 EBNF for the RIF-Core Condition Language

2.6.2 EBNF for the RIF-Core Rule Language

2.6.3 EBNF for RIF-Core Annotations

3 RIF-Core as a Specialization of RIF-PRD

3.1 Alphabet of RIF-Core

3.2 Terms of RIF-Core

3.3 Formulas of RIF-Core

3.4 Annotations and Documents

RIF-Core allows every term and formula to be optionally annotated in the same way as in RIF-PRD. The frame formulas that are allowed as part of an annotation must be syntactically correct for RIF-Core.

3.5 Well-formed Formulas

3.6 Rules and Groups

4 RIF-Core Semantics

RIF-Core is a syntactic subset of RIF-BLD, and the semantics of RIF-Core is identical to the semantics of RIF-BLD for that subset. RIF-Core is also a syntactic subset of RIF-PRD, and the semantics of RIF-Core is also identical to the semantics of RIF-PRD for that subset.

5 XML Serialization Syntax for RIF-Core

6 Safeness Criteria

RIF-Core is a syntactic subset of both RIF-BLD and RIF-PRD. The semantics of a RIF-Core formula is the same as the semantics given to it by RIF-BLD.

All RIF-Core documents are also syntactically valid RIF-PRD documents. However, some formulas may be unsafe and cannot be executed under the RIF-PRD operational semantics. Thus, in order to allow production rule systems and logic programming systems to interchange rules via RIF-Core, we restrict RIF-Core to safe rules so that the logical semantics of RIF-BLD and the operational fixed-point semantics of RIF-PRD coincide.

6.1 Safeness

Intuitively, safeness of rules guarantees that when performing reasoning in a forward-chaining manner, it is possible to find bindings for all the variables in the rule so that the condition can be evaluated.

To define safeness in the face of external predicates and functions, we define the notion of binding patterns, which are lists of the form (p₁, ..., p_n), such that p_i=b or p_i=u, for 1 ≤ i ≤ n. Intuitively, b stands for a "bound" and u stands for an "unbound" argument.

6.2 Strong Safeness (Informative)

While safeness guarantees the possibility to do forward chaining with the rules, it does not guarantee that it is possible to construct a finite grounding. For this purpose we define strong safeness.

The conformance clauses for RIF-Core only require conformance over safe rule sets as defined above. However, some rule engines, such as some Datalog engines, are only able to process rule sets which can be finitely grounded. For maximum interoperability with such systems it is recommended that RIF-Core producers restrict themselves to strongly safe rule sets where possible.

Let R be a set of safe rule implications φ :- ψ and let P be the set of pairs (p,n), where p is a predicate symbol and n is a nonnegative integer (an arity). For the purposes of the definitions in this section we view frames a[b -> c] and membership formulas a#b, respectively, as ternary and binary predicate symbols, and so (->,3), (#,2) ∈ P. Note that equality = does not appear in P.

We define the graph of variable dependencies of a set of atomic formulas A as a labeled directed graph G_R=(V, E, L), where the labeling function L maps edges to sets of external function and predicate symbols, V is the set of variables appearing in A, and E is the smallest set and L' is the smallest function such that for every variable ?V

• for every atomic formula ?V=t or t=?V in A and every variable ?V'≠?V appearing in t such that f₁, ..., f_n, 0 ≤ n, are the function symbols of the terms in t (including t itself) in which ?V' appears, (?V,?V') ∈ E and {f₁, ..., f_n} ∈ L'((?V,?V')), and
• for every external atomic formula External(f(t₁,...,t_n)) in A, every i ∈ {1,...,n} such that t_i=?V, every valid binding pattern (p₁, ..., p_n) of f such that p_i=u, and every variable ?V' appearing in some t_j such that p_i=b and f₁, ..., f_m, 0 ≤ m, are the function symbols of the terms in t_j in which ?V' appears, (?V,?V') ∈ E and {f₁, ..., f_m} ∈ L'((?V,?V')).

Finally, L is defined as: for every (e,e') ∈ E, L((e,e')) is the union of the minimal sets in L'((e,e')).

The dependency graph of a set of implications R is a labelled directed graph G_R=(V, E), where edges are triples (v,v',l) such that v, v' ∈ V and l is a set of external function and predicate symbols. V is defined as: for every (p,n) ∈ P and every integer i such that 1 ≤ i ≤ n, (p,n)/i ∈ V. E is the smallest set such that for every (p,n)/i ∈ V and every φ :- ψ in R such that there is an atomic subformula p(t₁,...,t_i,...,t_n) of φ, then for every variable ?V appearing in t_i:

• for every non-external and non-equality atomic formula with predicate symbol p' and m arguments in any A ∈ B_ψ and every j ∈ {1,...,m} such that a variable ?V'is the jth argument and there is a path from ?V to ?V' in the graph of variable dependencies of A and F is the union of the labels of the shortest path, ((p,n)/i,(p',m)/j, F ∪ {f₁,...,f_l}) ∈ E, where f₁, ..., f_l, 0 ≤ l, are the function symbols of the terms in t_i in which ?V appears.

7 Conformance Clauses

RIF-Core conformance is described in terms of semantics-preserving transformations.

8 Acknowledgements

This document is the product of the Rules Interchange Format (RIF) Working Group (see below) whose members deserve recognition for their time and commitment. The editors extend special thanks to Jos de Bruijn for his safeness definition and to: Jos de Bruijn, Leora Morgenstern, Christian de Sainte-Marie, Stella Mitchell and Changhai Ke for their thorough reviews and insightful discussions; the working group chairs, Chris Welty and Christian de Sainte-Marie, for their invaluable technical help and inspirational leadership; and W3C staff contact Sandro Hawke, a constant source of ideas, help, and feedback.

The regular attendees at meetings of the Rule Interchange Format (RIF) Working Group at the time of the publication were: Adrian Paschke (Freie Universitaet Berlin), Axel Polleres (DERI), Chris Welty (IBM), Christian de Sainte Marie (ILOG), Dave Reynolds (HP), Gary Hallmark (ORACLE), Harold Boley (NRC), Hassan Aït-Kaci (ILOG), John Hall (OMG), Jos de Bruijn (FUB), Leora Morgenstern (IBM), Michael Kifer (Stony Brook), Mike Dean (BBN), Sandro Hawke (W3C/MIT), and Stella Mitchell (IBM).

9 References

9.1 Normative References

9.2 Informational References

10 Appendix: XML Schema for RIF-Core

The namespace of RIF is http://www.w3.org/2007/rif#.

10.1 Condition Language

 <?xml version="1.0" encoding="UTF-8"?>
 
 <xs:schema 
  xmlns:xs="http://www.w3.org/2001/XMLSchema"
  xmlns="http://www.w3.org/2007/rif#"
  targetNamespace="http://www.w3.org/2007/rif#"
  elementFormDefault="qualified"
  version="Id: CoreCond.xsd, v. 0.8, 2009-04-29, hboley">
 
  <xs:annotation>
    <xs:documentation>
    This is the XML schema for the Condition Language as defined by
    the RIF Core Dialect.
    
    The schema is based on the following EBNF for the RIF-Core Condition Language
    (prepared for generalization to the RIF-BLD and RIF-PRD Condition Languages):
 
  FORMULA        ::= IRIMETA? 'And' '(' FORMULA* ')' |
                     IRIMETA? 'Or' '(' FORMULA* ')' |
                     IRIMETA? 'Exists' Var+ '(' FORMULA ')' |
                     ATOMIC |
                     IRIMETA? Equal |
                     IRIMETA? Member |
                     IRIMETA? 'External' '(' Atom ')'
  ATOMIC         ::= IRIMETA? (Atom | Frame)
  Atom           ::= UNITERM
  UNITERM        ::= Const '(' (TERM* ')'
  GROUNDUNITERM  ::= Const '(' (GROUNDTERM* ')'
  Equal          ::= TERM '=' TERM
  Member         ::= TERM '#' TERM
  Frame          ::= TERM '[' (TERM '->' TERM)* ']'
  TERM           ::= IRIMETA? (Const | Var | List | 'External' '(' Expr ')')
  GROUNDTERM     ::= IRIMETA? (Const | List | 'External' '(' 'Expr' '(' GROUNDUNITERM ')' ')')
  Expr           ::= UNITERM
  List           ::= 'List' '(' GROUNDTERM* ')'
  Const          ::= '"' UNICODESTRING '"^^' SYMSPACE | CONSTSHORT
  Name           ::= UNICODESTRING
  Var            ::= '?' UNICODESTRING
  SYMSPACE       ::= ANGLEBRACKIRI | CURIE
 
  IRIMETA        ::= '(*' IRICONST? (Frame | 'And' '(' Frame* ')')? '*)'
 
    </xs:documentation>
  </xs:annotation>
  
  <xs:group name="FORMULA">  
    <!--
  FORMULA        ::= IRIMETA? 'And' '(' FORMULA* ')' |
                     IRIMETA? 'Or' '(' FORMULA* ')' |
                     IRIMETA? 'Exists' Var+ '(' FORMULA ')' |
                     ATOMIC |
                     IRIMETA? Equal |
                     IRIMETA? Member |
                     IRIMETA? 'External' '(' Atom ')' 
    -->
    <xs:choice>
      <xs:element ref="And"/>
      <xs:element ref="Or"/>
      <xs:element ref="Exists"/>
      <xs:group ref="ATOMIC"/>
      <xs:element ref="Equal"/>
      <xs:element ref="Member"/>
      <xs:element name="External" type="External-FORMULA.type"/>
    </xs:choice>
  </xs:group>
  
  <xs:complexType name="External-FORMULA.type">
    <!-- sensitive to FORMULA (Atom) context-->
    <xs:sequence>
      <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
      <xs:element name="content" type="content-FORMULA.type"/>
    </xs:sequence>
  </xs:complexType>
  
  <xs:complexType name="content-FORMULA.type">
    <!-- sensitive to FORMULA (Atom) context-->
    <xs:sequence>
      <xs:element ref="Atom"/>
    </xs:sequence>
  </xs:complexType>
 
  <xs:element name="And">
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
        <xs:element ref="formula" minOccurs="0" maxOccurs="unbounded"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
  
  <xs:element name="Or">
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
        <xs:element ref="formula" minOccurs="0" maxOccurs="unbounded"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
  
  <xs:element name="Exists">
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
        <xs:element ref="declare" minOccurs="1" maxOccurs="unbounded"/>
        <xs:element ref="formula"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
  
  <xs:element name="formula">
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="FORMULA"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
  
  <xs:element name="declare">
    <xs:complexType>
      <xs:sequence>
        <xs:element ref="Var"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
 
  <xs:group name="ATOMIC">
    <!--
  ATOMIC         ::= IRIMETA? (Atom | Frame)
    -->
    <xs:choice>
      <xs:element ref="Atom"/>
      <xs:element ref="Frame"/>
    </xs:choice>
  </xs:group>
  
  <xs:element name="Atom">
    <!--
  Atom           ::= UNITERM
    -->
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="UNITERM"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>  
  
  <xs:group name="UNITERM">
    <!--
  UNITERM        ::= Const '(' (TERM* ')'
    -->
    <xs:sequence>
      <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
      <xs:element ref="op"/>
      <xs:element name="args" type="args-UNITERM.type"/>
    </xs:sequence>
  </xs:group>

  <xs:group name="GROUNDUNITERM">
    <!-- sensitive to ground terms
  GROUNDUNITERM        ::= Const '(' (GROUNDTERM* ')'
    -->
    <xs:sequence>
      <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
      <xs:element ref="op"/>
      <xs:element name="args" type="args-GROUNDUNITERM.type"/>
    </xs:sequence>
  </xs:group>
 
  <xs:element name="op">
    <xs:complexType>
      <xs:sequence>
        <xs:element ref="Const"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
  
  <xs:complexType name="args-UNITERM.type">
    <!-- sensitive to UNITERM (TERM) context-->
    <xs:sequence>
      <xs:group ref="TERM" minOccurs="0" maxOccurs="unbounded"/>
    </xs:sequence>
    <xs:attribute name="ordered" type="xs:string" fixed="yes"/>
  </xs:complexType>

  <xs:complexType name="args-GROUNDUNITERM.type">
    <!-- sensitive to GROUNDUNITERM (TERM) context-->
    <xs:sequence>
      <xs:group ref="GROUNDTERM" minOccurs="0" maxOccurs="unbounded"/>
    </xs:sequence>
    <xs:attribute name="ordered" type="xs:string" fixed="yes"/>
  </xs:complexType>


  <xs:element name="Equal">
    <!--
  Equal          ::= TERM '=' TERM
    -->
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
        <xs:element ref="left"/>
        <xs:element ref="right"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
 
  <xs:element name="left">
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="TERM"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
 
  <xs:element name="right">
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="TERM"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
 
  <xs:element name="Member">
    <!--
  Member         ::= TERM '#' TERM
    -->
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
        <xs:element ref="instance"/>
        <xs:element ref="class"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>

  <xs:element name="instance">
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="TERM"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
  
  <xs:element name="class">
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="TERM"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
  
  <xs:element name="Frame">
    <!--
  Frame          ::= TERM '[' (TERM '->' TERM)* ']'
    -->
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
        <xs:element ref="object"/>
        <xs:element name="slot" type="slot-Frame.type" minOccurs="0" maxOccurs="unbounded"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
 
  <xs:element name="object">
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="TERM"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
 
  <xs:complexType name="slot-Frame.type">
    <!-- sensitive to Frame (TERM) context-->
    <xs:sequence>
      <xs:group ref="TERM"/>
      <xs:group ref="TERM"/>
    </xs:sequence>
    <xs:attribute name="ordered" type="xs:string" fixed="yes"/>
  </xs:complexType>
 

 
  <xs:group name="TERM">  
    <!--
  TERM           ::= IRIMETA? (Const | Var | List | 'External' '(' Expr ')')
    -->
      <xs:choice>
         <xs:element ref="Const"/>
         <xs:element ref="Var"/>
         <xs:element ref="List"/>
         <xs:element name="External" type="External-TERM.type"/>
      </xs:choice>
  </xs:group>

  <xs:group name="GROUNDTERM">  
    <!--
  GROUNDTERM           ::= IRIMETA? (Const | List | 'External' '(' 'Expr' '(' GROUNDUNITERM ')' ')')
    -->
      <xs:choice>
         <xs:element ref="Const"/>
         <xs:element ref="List"/>
         <xs:element name="External" type="External-GROUNDUNITERM.type"/>
      </xs:choice>
  </xs:group>


 <xs:element name="List">  
    <!--
      List           ::= 'List' '(' GROUNDTERM* ')'
    -->
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="GROUNDTERM" minOccurs="0" maxOccurs="unbounded"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>


  <xs:complexType name="External-TERM.type">
    <!-- sensitive to TERM (Expr) context-->
    <xs:sequence>
      <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
      <xs:element name="content" type="content-TERM.type"/>
    </xs:sequence>
  </xs:complexType>

  <xs:complexType name="External-GROUNDUNITERM.type">
    <!-- sensitive to GROUNDTERM (Expr) context-->
    <xs:sequence>
      <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
      <xs:element name="content" type="content-GROUNDUNITERM.type"/>
    </xs:sequence>
  </xs:complexType>

  
  <xs:complexType name="content-TERM.type">
    <!-- sensitive to TERM (Expr) context-->
    <xs:sequence>
      <xs:element ref="Expr"/>
    </xs:sequence>
  </xs:complexType>

  <xs:complexType name="content-GROUNDUNITERM.type">
    <!-- sensitive to GROUNDTERM (Expr) context-->
    <xs:sequence>
      <xs:element name="Expr" type="content-GROUNDEXPR.type"/>
    </xs:sequence>
  </xs:complexType>

  <xs:complexType name="content-GROUNDEXPR.type">
    <!-- sensitive to GROUNDEXPR context-->
    <xs:sequence>
      <xs:element name="GROUNDUNITERM"/>
    </xs:sequence>
  </xs:complexType>



  <xs:element name="Expr">
    <!--
  Expr           ::= UNITERM
    -->
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="UNITERM"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>

  <xs:element name="Const">
    <!--
  Const          ::= '"' UNICODESTRING '"^^' SYMSPACE | CONSTSHORT
    -->
    <xs:complexType mixed="true">
      <xs:sequence>
        <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
      <xs:attribute name="type" type="xs:anyURI" use="required"/>
    </xs:complexType>
  </xs:element>
  
  <xs:element name="Name" type="xs:string">
    <!--
  Name           ::= UNICODESTRING
    -->
  </xs:element>
 
  <xs:element name="Var">
    <!--
  Var            ::= '?' UNICODESTRING
    -->
    <xs:complexType mixed="true">
      <xs:sequence>
        <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
 
  <xs:group name="IRIMETA">
    <!--
  IRIMETA   ::= '(*' IRICONST? (Frame | 'And' '(' Frame* ')')? '*)'
    -->
    <xs:sequence>
      <xs:element ref="id" minOccurs="0" maxOccurs="1"/>
      <xs:element ref="meta" minOccurs="0" maxOccurs="1"/>
    </xs:sequence>
  </xs:group>
 
  <xs:element name="id">
    <xs:complexType>
      <xs:sequence>
        <xs:element name="Const" type="IRICONST.type"/>   <!-- type="&rif;iri" -->
      </xs:sequence>
    </xs:complexType>
  </xs:element>
 
  <xs:element name="meta">
    <xs:complexType>
     <xs:choice>
       <xs:element ref="Frame"/>
       <xs:element name="And" type="And-meta.type"/>
     </xs:choice>
    </xs:complexType>
  </xs:element>
  
  <xs:complexType name="And-meta.type">
  <!-- sensitive to meta (Frame) context-->
    <xs:sequence>
      <xs:element name="formula" type="formula-meta.type" minOccurs="0" maxOccurs="unbounded"/>
    </xs:sequence>
  </xs:complexType>
 
  <xs:complexType name="formula-meta.type">
    <!-- sensitive to meta (Frame) context-->
    <xs:sequence>
      <xs:element ref="Frame"/>
    </xs:sequence>
  </xs:complexType>
  
  <xs:complexType name="IRICONST.type" mixed="true">
    <!-- sensitive to location/id context-->
    <xs:sequence/>
    <xs:attribute name="type" type="xs:anyURI" use="required" fixed="http://www.w3.org/2007/rif#iri"/>
  </xs:complexType>
  
 </xs:schema>

10.2 Rule Language

 <?xml version="1.0" encoding="UTF-8"?>
 
 <xs:schema 
  xmlns:xs="http://www.w3.org/2001/XMLSchema"
  xmlns="http://www.w3.org/2007/rif#"
  targetNamespace="http://www.w3.org/2007/rif#"
  elementFormDefault="qualified"
  version="Id: CoreRule.xsd, v. 0.8, 2009-04-16, hboley">
 
  <xs:annotation>
    <xs:documentation>
    This is the XML schema for the Rule Language as defined by
    the RIF Core Dialect.
    
    The schema is based on the following EBNF for the RIF-Core Rule Language
    (prepared for generalization to the RIF-BLD and RIF-PRD Rule Languages):
  
  Document  ::= IRIMETA? 'Document' '(' Base? Prefix* Import* Group? ')'
  Base      ::= 'Base' '(' IRI ')'
  Prefix    ::= 'Prefix' '(' Name IRI ')'
  Import    ::= IRIMETA? 'Import' '(' IRICONST PROFILE? ')'
  Group     ::= IRIMETA? 'Group' '(' (RULE | Group)* ')'
  RULE      ::= (IRIMETA? 'Forall' Var+ '(' CLAUSE ')') | CLAUSE
  CLAUSE    ::= Implies | ATOMIC
  Implies   ::= IRIMETA? (ATOMIC | 'And' '(' ATOMIC* ')') ':-' FORMULA
  PROFILE   ::= TERM
      
    Note that this is an extension of the syntax for the RIF-Core Condition Language (CoreCond.xsd).
    </xs:documentation>
  </xs:annotation>
 
  <!-- The Rule Language includes the Condition Language from the same directory -->
  <xs:include schemaLocation="CoreCond.xsd"/>
 
  <xs:element name="Document">
    <!--
  Document  ::= IRIMETA? 'Document' '(' Base? Prefix* Import* Group? ')'
    -->
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
        <xs:element ref="directive" minOccurs="0" maxOccurs="unbounded"/>
        <xs:element ref="payload" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
 
  <xs:element name="directive">
    <!--
  Base and Prefix represented directly in XML
    -->
    <xs:complexType>
      <xs:sequence>
        <xs:element ref="Import"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
 
  <xs:element name="payload">
    <xs:complexType>
      <xs:sequence>
        <xs:element ref="Group"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
  
  <xs:element name="Import">
    <!--
  Import    ::= IRIMETA? 'Import' '(' IRICONST PROFILE? ')'
    -->
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/> 
        <xs:element ref="location"/>
        <xs:element ref="profile" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
 
  <xs:element name="location">
    <xs:complexType>
      <xs:sequence>
        <xs:element name="Const" type="IRICONST.type"/>   <!-- type="&rif;iri" -->
      </xs:sequence>
    </xs:complexType>
  </xs:element>
 
  <xs:element name="profile">
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="TERM"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
  
  <xs:element name="Group">
    <!--
  Group     ::= IRIMETA? 'Group' '(' (RULE | Group)* ')'
    -->
    <xs:complexType>
     <xs:sequence>
      <xs:group ref="Group.content"/>
      </xs:sequence> 
    </xs:complexType>
  </xs:element>
 
 <xs:group name="Group.content">
     <xs:sequence>
        <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
        <xs:element ref="sentence" minOccurs="0" maxOccurs="unbounded"/>
      </xs:sequence>
 </xs:group>



  <xs:element name="sentence">
   <xs:complexType>
     <xs:choice>
       <xs:group ref="RULE"/>
       <xs:element ref="Group"/>
     </xs:choice>
   </xs:complexType>
 </xs:element>
  
  <xs:group name="RULE">
    <!--
  RULE      ::= (IRIMETA? 'Forall' Var+ '(' CLAUSE ')') | CLAUSE
    -->
    <xs:choice>
      <xs:element ref="Forall"/>
      <xs:group ref="CLAUSE"/>
    </xs:choice>
  </xs:group>
 
  <xs:element name="Forall">
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="Forall.content"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>

  <xs:group name="Forall.content">  
      <xs:sequence>
        <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
        <xs:element ref="declare" minOccurs="1" maxOccurs="unbounded"/>
        <!-- different from formula in And, Or and Exists -->
        <xs:element name="formula">
          <xs:complexType>
            <xs:group ref="CLAUSE"/>
          </xs:complexType>
        </xs:element>
      </xs:sequence>
  </xs:group>
 

  <xs:group name="CLAUSE">  
    <!--
  CLAUSE   ::= Implies | ATOMIC
    -->
    <xs:choice>
      <xs:element ref="Implies"/>
      <xs:group ref="ATOMIC"/>
    </xs:choice>
  </xs:group>
  
  <xs:element name="Implies">
    <!--
  Implies   ::= IRIMETA? (ATOMIC | 'And' '(' ATOMIC* ')') ':-' FORMULA
    -->
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/>
        <xs:element ref="if"/>
        <xs:element ref="then"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
 
  <xs:element name="if">
    <xs:complexType>
      <xs:sequence>
        <xs:group ref="FORMULA"/>
      </xs:sequence>
    </xs:complexType>
  </xs:element>
  
  <xs:element name="then">
    <xs:complexType>
     <xs:sequence>
       <xs:group ref="then.content"/>
     </xs:sequence>
    </xs:complexType>
  </xs:element>

  <xs:group name="then.content">  
     <xs:choice>
       <xs:group ref="ATOMIC"/>
       <xs:element name="And" type="And-then.type"/>
     </xs:choice>
  </xs:group>

 
  <xs:complexType name="And-then.type">
    <!-- sensitive to then (ATOMIC) context-->
    <xs:sequence>
      <xs:element name="formula" type="formula-then.type" minOccurs="0" maxOccurs="unbounded"/>
    </xs:sequence>
  </xs:complexType>
 
  <xs:complexType name="formula-then.type">
    <!-- sensitive to then (ATOMIC) context-->
    <xs:sequence>
      <xs:group ref="ATOMIC"/>
    </xs:sequence>
  </xs:complexType>
   
 </xs:schema>