FOL RuleML: The First-Order Logic RuleML Language

Abstract

Status of this document

1. Introduction

First-Order Logic RuleML (FOL RuleML) is introduced here on the basis of combining Quantifier RuleML and Disjunctive RuleML. This sublanguage combination is then enriched by further connectives, notably by classical negation, for achieving FOL RuleML. The markup language for first-order logic introduced here is itself proposed as a central RuleML sublanguage, extending the design of RuleML 0.87]. It will also benefit other sublanguages towards RuleML 0.9, such as the current Horn logic markup.

A notion of 'query' will be used in this paper that corresponds to what has often been named 'goal' in the AI literature. A query in this sense encompasses a formula that can be proved either by direct retrieval or by a general (here, FOL) deduction (in FOL not necessarily based on ultimate direct retrievals). Other work on query languages has focussed on retrieval, and has generalized complementary aspects such as the expressiveness of query patterns, aggregates, etc. In particular, the W3C RDF Data Access Working Group is defining generalized retrieval through multiple-valued graph pattern matching. It will be interesting to see how this could be simulated by, or combined with, the FOL queries discussed here. Another connection with W3C's DAWG is RuleML's striped syntax, motived by RDF, which in this paper will be carried over to FOL RuleML, and will be abridged via StripeSkipping.

Explicit quantifiers, 'Forall' and 'Exists', are now optionally provided for FOL purposes. These quantifiers have been requested by RuleML participants as well as SWRL observers including Drew McDermott, and are essential for all full FOL languages such as DRS, SCL, and FOL RuleML. We will also optionally provide an abbreviation syntax for regarding certain free variables as universally quantified variables, which is more explicit than the convention of Prolog/LP and many other (theorem-proving) systems: A 'closure' attribute on clauses can be set to "universal" (or "existential"); similarly, for entire rulebases.

In the spirit of the logic in 'FOL RuleML', the conjoined clauses of a rulebase are connected by an explicit 'And'. FOL RuleML also allows a corresponding 'Or', for disjoined clauses. Either of these parent connectives can have attributes for expressing properties of contained clauses. In particular, the free-variable convention of the clausal normal form in theorem provers is expressed explicitly by the attribute setting innerclose="universal", universally closing off clauses occurring as subformulas in the parent 'And'/'Or', i.e. acting as if all of its contained clauses would have the attribute setting closure="universal".

RuleML 0.87 top-level elements ('Imp', 'Fact', and -- still -- 'Query') -- directly below a rulebase -- can contain extra information such as a rule label (also planned: a rule salience etc.). This information is now also offered for sublevel elements, e.g. to refer to the elements of a local rulebase. We can thus avoid a top-level/sublevel duplication for connectives such as through a previously proposed 'Imp'/'Implies' distinction.

RuleML files and messages strive for a strict separation of declarative content from procedural performatives, as pioneered by KQML. FOL RuleML is focused on the syntax and semantics of the FOL content language, specifying the FOL content formulas that can go into any performative of any other system that refers to the FOL RuleML namespace: these FOL formulas acquire their pragmatics from the enclosing performative context. Just for transmitting FOL RuleML content under a single XML root, without specifying what should be done with the content, we introduce a neutral performative, called 'Consider'. Appendix 1 gives a complete example, which uses the Horn subset of FOL to demonstrate a minimal XML wrapping of FOL RuleML content into performatives. Using FOL RuleML we may have, e.g., the same 'And' of clauses as the content that can be wrapped by, e.g., a KQML-'tell'-like 'Assert' performative. Appendix 2 gives an example of an 'Assert'-'And' nesting, which corresponds to a 'Rulebase' in RuleML 0.87. Since FOL RuleML permits implications as queries, the same content could moreover be wrapped by a 'Query' performative. Appendix 3 gives an FOL query example.

In this paper the performatives 'Consider', 'Assert', and 'Query' are the only examples used as wrappers (shown as blue-colored boxes) around FOL RuleML content (shown as white-colored boxes). Future RuleML work may contemplate a further performative wrapping an FOL formula used as an integrity constraint, which could be called 'Sustain'. Also, a 'Retract' performative, similar to KQML's 'untell', wrapping an FOL formula to be deleted, is relevant to some RuleML sublanguages. Certain performatives such as 'Query' can appear directly as the root of an XML file or message (e.g., the explicit 'Query' in Appendix 2) or could be generated by processors (e.g., a top-down interpreter) from content such as an 'Implies' rule (e.g., extracting the query implicit in the body conjunction of the 'Implies' in Appendix 1) to form a new XML file or message. However, the latter option is outside the scope of the RuleML language specification.

Since the Semantic Web Services Initiative SWSI is working in areas related to performatives, and is planning to use FOL RuleML as an FOL content language, we envisage a close RuleML/SWSI collaboration in finishing the FOL RuleML content language and in defining RuleML/SWSI performatives. The second aspect of this collaboration goes much beyond FOL RuleML since performatives involve other RuleML sublanguages such as Object-Oriented RuleML (OO RuleML) and are close to efforts in Reaction RuleML (Reaction TG). Also, previous work on OWL-QL (DQL) will be relevant here. One issue to be solved is how to build on Web Services standards such as SOAP when enriching the 'content' argument of performatives by further sublements for the receiver, sender, in-reply-to, etc. (which can become slots in OO RuleML).

The RuleML/SWSI/DAWG collaboration will be simplified by the modularity stemming from the separation of FOL RuleML content and RuleML/SWSI/DAWG/... performatives. The Syntax and Semantics of FOL RuleML is normative only w.r.t. the (white-boxed) FOL content language.

2. Explicit Quantifiers

In the Quantifier RuleML module, explicit ('Forall' and 'Exists') quantifiers are allowed on all levels of rulebase elements, in particular immediately above and anywhere within implication elements.

For example, the RuleML 0.87 'own' rule (where the 'Imp' element happens to contain no rule-label child)

<Imp>
  <head>
    <Atom>
      <Rel>own</Rel>
      <Var>person</Var>
      <Var>object</Var>
    </Atom>
  </head>
  <body>
    <And>
      <Atom>
        <Rel>buy</Rel>
        <Var>person</Var>
        <Var>merchant</Var>
        <Var>object</Var>
      </Atom>
      <Atom>
        <Rel>keep</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
    </And>
  </body>
</Imp>

will be rewritten with an 'Implies' connective (whose 'closure' attribute will normally be generated from the 'innerclose' attribute of the parent connective, usually an 'And'):

<Implies closure="universal">
  <head>
    <Atom>
      <Rel>own</Rel>
      <Var>person</Var>
      <Var>object</Var>
    </Atom>
  </head>
  <body>
    <And>
      <Atom>
        <Rel>buy</Rel>
        <Var>person</Var>
        <Var>merchant</Var>
        <Var>object</Var>
      </Atom>
      <Atom>
        <Rel>keep</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
    </And>
  </body>
</Implies>

The appendixes illustrate an abridged version of this rule in context with the 'closure' attribute lifted to an 'innerclose' attribute.

This can be expanded to an 'own' rule with an explicit quantifier (a 'Forall' quantifier) extracting all variables that occur free in the 'closure'-attributed 'Implies'-connective formula. The extracted variables are put under 'declare' roles, and the 'closure'-less 'Implies' is put under a 'formula' role, as follows:

<Forall>
  <declare><Var>person</Var></declare>
  <declare><Var>merchant</Var></declare>
  <declare><Var>object</Var></declare>
  <formula>
    <Implies>
      <head>
        <Atom>
          <Rel>own</Rel>
          <Var>person</Var>
          <Var>object</Var>
        </Atom>
      </head>
      <body>
        <And>
          <Atom>
            <Rel>buy</Rel>
            <Var>person</Var>
            <Var>merchant</Var>
            <Var>object</Var>
          </Atom>
          <Atom>
            <Rel>keep</Rel>
            <Var>person</Var>
            <Var>object</Var>
          </Atom>
        </And>
      </body>
    </Implies>
  </formula>
</Forall>

We will use the convention for role skipping of RuleML 0.87, which allows us to omit the 'declare' and 'formula' roles, as follows (where 'Var' type tags as direct child elements of 'Forall' get their role tag reconstructed as 'declare', while any other type tag gets reconstructed as 'formula'):

<Forall>
  <Var>person</Var>
  <Var>merchant</Var>
  <Var>object</Var>
  <Implies>
    <head>
      <Atom>
        <Rel>own</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
    </head>
    <body>
      <And>
        <Atom>
          <Rel>buy</Rel>
          <Var>person</Var>
          <Var>merchant</Var>
          <Var>object</Var>
        </Atom>
        <Atom>
          <Rel>keep</Rel>
          <Var>person</Var>
          <Var>object</Var>
        </Atom>
      </And>
    </body>
  </Implies>
</Forall>

This itself can be considered as the prenex normal form of an 'own' rule with an explicit outer 'Forall' and an explicit inner (body-side) 'Exists' quantifier:

<Forall>
  <Var>person</Var>
  <Var>object</Var>
  <Implies>
    <head>
      <Atom>
        <Rel>own</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
    </head>
    <body>
      <Exists>
        <Var>merchant</Var>
        <And>
          <Atom>
            <Rel>buy</Rel>
            <Var>person</Var>
            <Var>merchant</Var>
            <Var>object</Var>
          </Atom>
          <Atom>
            <Rel>keep</Rel>
            <Var>person</Var>
            <Var>object</Var>
          </Atom>
        </And>
      </Exists>
    </body>
  </Implies>
</Forall>

The 'Var' declaration part of quantified formulas like the above also provides a natural place to introduce types/sorts for those variables (once) as called for by OO RuleML.

Because of the unorderedness of roles, here 'head' and 'body' roles, the last but first version is syntactically equivalent to

<Forall>
  <Var>person</Var>
  <Var>merchant</Var>
  <Var>object</Var>
  <Implies>
    <body>
      <And>
        <Atom>
          <Rel>buy</Rel>
          <Var>person</Var>
          <Var>merchant</Var>
          <Var>object</Var>
        </Atom>
        <Atom>
          <Rel>keep</Rel>
          <Var>person</Var>
          <Var>object</Var>
        </Atom>
      </And>
    </body>
    <head>
      <Atom>
        <Rel>own</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
    </head>
  </Implies>
</Forall>

The role skipping of RuleML 0.87 now allows us to omit the 'head' and 'body' roles, as suggested by the type tag 'Implies' (as opposed to a -- not currently existing -- type tag 'IsImpliedBy'):

<Forall>
  <Var>person</Var>
  <Var>merchant</Var>
  <Var>object</Var>
  <Implies>
    <And>
      <Atom>
        <Rel>buy</Rel>
        <Var>person</Var>
        <Var>merchant</Var>
        <Var>object</Var>
      </Atom>
      <Atom>
        <Rel>keep</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
    </And>
    <Atom>
      <Rel>own</Rel>
      <Var>person</Var>
      <Var>object</Var>
    </Atom>
  </Implies>
</Forall>

While the above examples are just different ways of expressing a Horn rule using explicit quantifiers, the following example uses them for added FOL expressiveness. This new rule about claiming, both of whose 'Implies' elements contain a rule label, leaves the outer 'Forall' implicit and employs an explicit inner (body-side) 'Forall' over an embedded 'Implies':

<Implies closure="universal">
  <rlab><Ind>claiming-through-disclaimers</Ind></rlab>
  <head>
    <Atom>
      <Rel>claim</Rel>
      <Var>person</Var>
      <Var>object</Var>
    </Atom>
  </head>
  <body>
    <And>
      <Forall>
        <Var>x</Var>
        <Implies>
	  <rlab><Ind>disclaiming-of-other-persons</Ind></rlab>
          <body>
            <Atom>
              <Rel>unequal</Rel>
              <Var>x</Var>
              <Var>person</Var>
            </Atom>
          </body>
          <head>
            <Atom>
              <Rel>disclaim</Rel>
              <Var>x</Var>
              <Var>object</Var>
            </Atom>
          </head>
        </Implies>
      </Forall>
      <Atom>
        <Rel>keep</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
    </And>
  </body>
</Implies>

In a similar way, the RuleML 'keep' fact (where the 'Fact' element contains a rule-label and a 'head' child)

<Fact>
  <rlab><Ind>Mary-keeps-everything</Ind></rlab>
  <head>
    <Atom>
      <Rel>keep</Rel>
      <Ind>Mary</Ind>
      <Var>object</Var>
    </Atom>
  </head>
</Fact>

or, using the ('head') role reconstruction of RuleML 0.87,

<Fact>
  <rlab><Ind>Mary-keeps-everything</Ind></rlab>
  <Atom>
    <Rel>keep</Rel>
    <Ind>Mary</Ind>
    <Var>object</Var>
  </Atom>
</Fact>

will be rewritten as a 'keep' 'Atom' (whose 'closure' attribute will normally be generated from the 'innerclose' attribute of the parent connective, usually an 'And'):

<Atom closure="universal">
  <rlab><Ind>Mary-keeps-everything</Ind></rlab>
  <Rel>keep</Rel>
  <Ind>Mary</Ind>
  <Var>object</Var>
</Atom>

The appendixes illustrate a version of this fact in context with the 'closure' attribute lifted to an 'innerclose' attribute.

This can be expanded to a 'keep' atom with an explicit quantifier (a 'Forall' quantifier) binding the declared free variable of the atomic formula, as follows:

<Forall>
  <Var>object</Var>
  <Atom>
    <rlab><Ind>Mary-keeps-everything</Ind></rlab>
    <Rel>keep</Rel>
    <Ind>Mary</Ind>
    <Var>object</Var>
  </Atom>
</Forall>

3. Head Disjunctions

Disjunctions in the head of clauses and in all sublevel positions are allowed in the Disjunctive RuleML module.

For example, the RuleML 'own' rule

<Implies closure="universal">
  <head>
    <Atom>
      <Rel>own</Rel>
      <Var>person</Var>
      <Var>object</Var>
    </Atom>
  </head>
  <body>
    <And>
      <Atom>
        <Rel>buy</Rel>
        <Var>person</Var>
        <Var>merchant</Var>
        <Var>object</Var>
      </Atom>
      <Atom>
        <Rel>keep</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
    </And>
  </body>
</Implies>

can be changed into a disjunctive ('own'-or-'relinquish') rule as follows:

<Implies closure="universal">
  <head>
    <Or>
      <Atom>
        <Rel>own</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
      <Atom>
        <Rel>relinquish</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
    </Or>
  </head>
  <body>
    <Atom>
      <Rel>buy</Rel>
      <Var>person</Var>
      <Var>merchant</Var>
      <Var>object</Var>
    </Atom>
  </body>
</Implies>

In a similar manner, we permit a disjunctive fact that could be derived by the above rule and a suitable 'buy' fact:

<Or>
  <Atom>
    <Rel>own</Rel>
    <Ind>Mary</Ind>
    <Ind>XMLBible</Ind>
  </Atom>
  <Atom>
    <Rel>relinquish</Rel>
    <Ind>Mary</Ind>
    <Ind>XMLBible</Ind>
  </Atom>
</Or>

4. Combined Quantifiers and Disjunctions

Explicit ('Forall' and 'Exists') quantifiers can be combined with disjunctions in the head of clauses and in all sublevel positions.

For example, this is a disjunctive ('claim'-or-'relinquish') rule with an inner (body-side) explicit quantifier (a 'Forall') over an embedded 'implies':

<Implies closure="universal">
  <rlab><Ind>claiming-or-relinquishing-through-disclaimers</Ind></rlab>
  <head>
    <Or>
      <Atom>
        <Rel>claim</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
      <Atom>
        <Rel>relinquish</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
    </Or>
  </head>
  <body>
    <Forall>
      <Var>x</Var>
      <Implies>
      	<rlab><Ind>disclaiming-of-other-persons</Ind></rlab>
        <body>
          <Atom>
            <Rel>unequal</Rel>
            <Var>x</Var>
            <Var>person</Var>
          </Atom>
        </body>
        <head>
          <Atom>
            <Rel>disclaim</Rel>
            <Var>x</Var>
            <Var>object</Var>
          </Atom>
        </head>
      </Implies>
    </Forall>
  </body>
</Implies>

5. Equivalence

Besides reducing 'Equivalent' to a pair of conjoined converse 'Implies', we also allow to represent it directly, modeled on 'Implies', but with a symmetric 'torso' role that combines the asymmetric 'head' and 'body' roles.

For example, without introducing a new connective, a pair of conjoined converse 'Implies' formulas can express an 'own'/'belongs' equivalence as follows:

<Forall>
  <Var>person</Var>
  <Var>object</Var>
  <And>
    <Implies>
      <body>
        <Atom>
          <Rel>own</Rel>
          <Var>person</Var>
          <Var>object</Var>
        </Atom>
      </body>
      <head>
        <Atom>
          <Rel>belongs</Rel>
          <Var>object</Var>
          <Var>person</Var>
        </Atom>
      </head>
    </Implies>
    <Implies>
      <body>
        <Atom>
          <Rel>belongs</Rel>
          <Var>object</Var>
          <Var>person</Var>
        </Atom>
      </body>
      <head>
        <Atom>
          <Rel>own</Rel>
          <Var>person</Var>
          <Var>object</Var>
        </Atom>
      </head>
    </Implies>
  </And>
</Forall>

However, with the 'Equivalent' connective, this 'own'/'belongs' equivalence can be shortened into a single rule thus:

<Forall>
  <Var>person</Var>
  <Var>object</Var>
  <Equivalent>
    <torso>
      <Atom>
        <Rel>own</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
    </torso>
    <torso>
      <Atom>
        <Rel>belongs</Rel>
        <Var>object</Var>
        <Var>person</Var>
      </Atom>
    </torso>
  </Equivalent>
</Forall>

Because of the symmetry of equivalence, the 'torso' role can be trivially reconstructed (in the way the 'role' metarole is reconstructed in RuleML 0.87), so that the 'own'/'belongs' rule can be further shortened thus:

<Forall>
  <Var>person</Var>
  <Var>object</Var>
  <Equivalent>
    <Atom>
      <Rel>own</Rel>
      <Var>person</Var>
      <Var>object</Var>
    </Atom>
    <Atom>
      <Rel>belongs</Rel>
      <Var>object</Var>
      <Var>person</Var>
    </Atom>
  </Equivalent>
</Forall>

6. Negation

Classical negation in FOL RuleML is introduced as a 'Neg' element. (This is strictly separated from other RuleML sublanguages where partial-logic extensions to 'Neg' are permitted, from further sublanguages introducing the as-failure 'Naf' element, and from sublanguages also allowing certain 'Naf'/'Neg' combinations.)

For instance, in the earlier FOL-expressive example, the 'unequal' relation can be replaced by a 'Not'-negated 'equal' relation (we immediately omit its trivially reconstructed single-argument role, 'strong'):

<Implies closure="universal">
  <rlab><Ind>claiming-through-disclaimers</Ind></rlab>
  <head>
    <Atom>
      <Rel>claim</Rel>
      <Var>person</Var>
      <Var>object</Var>
    </Atom>
  </head>
  <body>
    <And>
      <Forall>
        <Var>x</Var>
        <Implies>
          <rlab><Ind>disclaiming-of-other-persons</Ind></rlab>
          <body>
            <Neg>
	      <Atom>
                <Rel>equal</Rel>
                <Var>x</Var>
                <Var>person</Var>
              </Atom>
	    </Neg>
          </body>
          <head>
            <Atom>
              <Rel>disclaim</Rel>
              <Var>x</Var>
              <Var>object</Var>
            </Atom>
          </head>
        </Implies>
      </Forall>
      <Atom>
        <Rel>keep</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
    </And>
  </body>
</Implies>

The tag 'Neg' may be renamed into 'Not', as detailed in the Issues List, item 9.

7. Complex Terms

While the 'Atom' element was so far restricted to the constructorless FOL subset, it will now be extended for complex terms as also used in RuleML's Hornlog sublanguage. First, besides 'Ind' or 'Var' children, an 'Atom' can now contain 'Cterm' child elements. Similarly, a complex term or 'Cterm' is then defined to apply a constructor or 'Ctor' child element to 'Ind', 'Var', or (recursively) 'Cterm' child elements.

For instance, a 'Cterm' constructing a 'book' from an author, a title, and a year can be used within an 'Atom' expressing a 'buy' fact relating a buyer, a seller, and this book:

<Atom>
  <Rel>buy</Rel>
  <Ind>Mary</Ind>
  <Ind>John</Ind>
  <Cterm>
    <Ctor>book</Ctor>
    <Ind>Elliotte Rusty Harold</Ind>
    <Ind>XML Bible</Ind>
    <Ind>2001</Ind>
  </Cterm>
</Atom>

8. Syntax and Semantics

The FOL RuleML syntax defines the connectives co-recursively in the usual FOL manner so that arbitrary nestings are allowed.

The shortened form of the FOL RuleML content language (for simplicity omitting the rlab role on atoms and connectives) is defined through the following normative DTD grammar, where the ENTITY declaration handles the markupless recursive non-terminal 'foformula':

<!ENTITY % foformula "(Atom | And | Or | Neg | Implies | Equivalent | Forall | Exists)">

<!ELEMENT Atom (Rel, (Ind | Var | Cterm)*)>
<!ELEMENT Cterm (Ctor, (Ind | Var | Cterm)*)>

<!ELEMENT And ((%foformula;)*)>
<!ELEMENT Or ((%foformula;)*)>
<!ELEMENT Neg (%foformula;)>
<!ELEMENT Implies (%foformula;, %foformula;)>
<!ELEMENT Equivalent (%foformula;, %foformula;)>

<!ELEMENT Forall (Var+, %foformula;)>
<!ELEMENT Exists (Var+, %foformula;)>

<!ELEMENT Ind  (#PCDATA)>
<!ELEMENT Var  (#PCDATA)>
<!ELEMENT Rel  (#PCDATA)>
<!ELEMENT Ctor  (#PCDATA)>

<!ATTLIST And innerclose (universal | existential) #IMPLIED>
<!ATTLIST Or innerclose (universal | existential) #IMPLIED>
<!ATTLIST Neg innerclose (universal | existential) #IMPLIED>

<!ATTLIST Atom closure (universal | existential) #IMPLIED>
<!ATTLIST Implies closure (universal | existential) #IMPLIED>
<!ATTLIST Equivalent closure (universal | existential) #IMPLIED>

Note that the attributes 'innerclose' and 'closure' are specified, respectively, for boolean ('And'/'Or'/'Neg') and clause ('Atom'/'Implies'/'Equivalent') elements with the keyword #IMPLIED, which makes them optional. Since the 'closure' attribute is the fundamental one (cf. Appendix 1, Document 1), on which the 'innerclose' attribute is based (cf. Appendix 1, Document 1), users can opt to employ 'closure' without employing 'innerclose', but not the other way round. The 'closure' attribute specifies a universal or existential closure over all variables that occur free in its clause element. The 'innerclose' attribute specifies correspondingly valued 'closure'/'innerclose' attributes for all 'closure'/'innerclose'-less clauses/booleans occurring directly in its boolean element. It tells applications to propagate the value v ("universal" or "existential") found in a innerclose=v of a boolean element to their direct subelements, inserting closure=v into any clause that does not already have a 'closure' attribute, and recursively inserting innerclose=v into any boolean that does not already have an 'innerclose' attribute. This also allows the explicit 'Forall'/'Exists' quantification over the variables in a boolean or clause element that does not use an 'innerclose' or 'closure' attribute, respectively.

The above DTD is available for validation tests at http://www.ruleml.org/fol/fol-monolith.dtd (browse with, e.g., Firefox or the IE 6.0.2800.1106 version that has the appropriate SP1 Q8????? updates). For example, Richard Goerwitz' STG Validator succeeds with the content language conjunction of the appendixes:

Text:

While 'And' is distinguished here (after 'DOCTYPE') as the document root, 'Or' and the other connectives can be designated as the root, too.

The neutral 'Consider' performative, as illustrated in Appendix 1, for transmitting FOL RuleML content under a single document root can be added to the above DTD via the following non-normative line:

The usual formula simplifications and transformations can be applied to these FOL RuleML formulas (e.g., leading to normal forms). For example, 'And' is often needed in the body and (e.g., for SWRL) in the head of clauses, but an 'And' (such as a conjunction of converse 'Implies' elements) is not required on a rulebase top-level that is itself an 'And' of child formulas. As another example, applying de Morgan, a top-level 'Or' of 'Implies' (and 'Equivalent') rules can be re-expressed via the classical negation of an 'And' of the classically negated rules.

The tag 'Neg' may be renamed into 'Not', as detailed in the Issues List, item 9.

9. Slotted FOL RuleML

N-ary relations with named/keyed arguments can be expressed in FOL RuleML with slots, following OO RuleML. The Abstract Syntax sample formula with a named n-ary relationship from Peter Patel-Schneider's Proposal for a SWRL Extension to First-Order Logic is:

forall( I-variable(x ex:FantasyNovel)
      Purchase(buyer=ex:peter seller=ex:amazon object=x quantity="1"^^xsd:int))

Here is its XML Syntax in Slotted FOL RuleML (with two XML attributes:
'type' for webized classes and 'wid' and for webized individuals):

<Forall>
  <Var type="ex:FantasyNovel">x</Var>
  <Atom>
    <Rel>Purchase</Rel>
    <slot>
      <Ind>buyer</Ind>
      <Ind wid="ex:peter"/>
    </slot>
    <slot>
      <Ind>seller</Ind>
      <Ind wid="ex:amazon"/>
    </slot>
    <slot>
      <Ind>object</Ind>
      <Var>x</Var>
    </slot>
    <slot>
      <Ind>quantity</Ind>
      <Ind type="xsd:int">1</Ind>
    </slot>
  </Atom>
</Forall>

10. SWRL FOL RuleML

SWRL FOL and FOL RuleML can be joined to SWRL FOL RuleML by either adding RuleML extensions such as n-ary relations to SWRL FOL or by adding SWRL extensions such as data-valued properties to FOL RuleML.

Peter Patel-Schneider's Proposal for a SWRL Extension to First-Order Logic can provide the direct model-theoretic semantics for the SWRL FOL subset of SWRL FOL RuleML.

Using FOL RuleML as described here, the example assertion in XML concrete syntax of Peter Patel-Schneider's above document becomes the following SWRL FOL RuleML example (where the 'owlx:name' value has been webized and 'owlx:Annotation' has been left unchanged):

<ruleml:Assert owlx:name="#Example">
  <owlx:Annotation>
    <owlx:Label>Example Rule for Expository Purposes</owlx:Label>
  </owlx:Annotation>

  <ruleml:Forall>
    <ruleml:Var type="Person">x1</ruleml:Var>
    <ruleml:Var type="Parent">x2</ruleml:Var>
    <ruleml:Var type="Person">x3</ruleml:Var>
    <ruleml:Var type="xsd:int">x4</ruleml:Var>
    <ruleml:And>
      <swrlx:individualPropertyAtom swrlx:property="hasParent">
        <ruleml:Var>x1</ruleml:Var>
        <ruleml:Var>x2</ruleml:Var>
      </swrlx:individualPropertyAtom>
      <swrlx:individualPropertyAtom swrlx:property="hasBrother"> 
        <ruleml:Var>x2</ruleml:Var>
        <ruleml:Var>x3</ruleml:Var>
      </swrlx:individualPropertyAtom>
      <swrlx:datatypePropertyAtom swrlx:property="hasAge"> 
        <ruleml:Var>x2</ruleml:Var>
        <ruleml:Var>x4</ruleml:Var>
      </swrlx:datatypePropertyAtom>
    </ruleml:And>
  </ruleml:Forall>

</ruleml:Assert>

Notice that with rulebases becoming 'And' assertions, each fact inside becoming an 'Atom' (in SWRL, an 'individualPropertyAtom' or a 'datatypePropertyAtom'), this example can be viewed either as an asserted formula whose connective is an 'And' or as a rulebase of three facts grouped together by an 'And' connective.

Generally, in both views, FOL RuleML and SWRL FOL RuleML only permit one 'Assert' root per file or message. (Other, clearly distinct, RuleML sublanguages, studied by the Reaction TG, also permit for incremental, even dynamic, 'Assert' performatives, as required, e.g., for production rules.)

11. Built-ins for SWRL FOL RuleML

The SWRL Built-ins, being designed in a declarative fashion and used through a specialized 'Atom' ('swrlx:builtinAtom'), can be easily extended to SWRL FOL RuleML.

This is a test query using the 'swrlb:greaterThanOrEqual' built-in for SWRL FOL RuleML:

<ruleml:Query owlx:name="#Test">
  <owlx:Annotation>
    <owlx:Label>Test Query for Expository Purposes</owlx:Label>
  </owlx:Annotation>

  <ruleml:Exists>
    <ruleml:Var type="Person">x1</ruleml:Var>
    <ruleml:Var type="xsd:int">x2</ruleml:Var>
    <ruleml:And>
      <swrlx:datatypePropertyAtom swrlx:property="hasAge"> 
        <ruleml:Var>x1</ruleml:Var>
        <ruleml:Var>x2</ruleml:Var>
      </swrlx:datatypePropertyAtom>
      <swrlx:builtinAtom swrlx:builtin="&swrlb;#greaterThanOrEqual"> 
        <ruleml:Var>x1</ruleml:Var>
        <ruleml:Var>x2</ruleml:Var>
      </swrlx:builtinAtom>
    </ruleml:And>
  </ruleml:Exists>

</ruleml:Query>

12. The FOL XSDs

To obtain the Schema of RuleML 0.9 we will incorporate the FOL modules along with other ones into the correspondingly adapted current XML Schema. The monolith DTD grammar of Syntax and Semantics and the monolith XSD derived from it for the XML Concrete Syntax of SWRL FOL will guide the modular XSD specification.

13. Appendix 1: 'own' Example as Universal 'Consider'

Document 1 -- Universally Closed 'And' Elements in 'Consider' Wrapper:

<Consider>

  <And innerclose="universal">

    <Implies>
      <And>
        <Atom>
          <Rel>buy</Rel>
          <Var>person</Var>
          <Var>merchant</Var>
          <Var>object</Var>
        </Atom>
        <Atom>
          <Rel>keep</Rel>
          <Var>person</Var>
          <Var>object</Var>
        </Atom>
      </And>
      <Atom>
        <Rel>own</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
    </Implies>
    
    <Atom>
      <Rel>buy</Rel>
      <Ind>Mary</Ind>
      <Ind>John</Ind>
      <Cterm>
        <Ctor>book</Ctor>
        <Ind>Elliotte Rusty Harold</Ind>
        <Ind>XML Bible</Ind>
        <Ind>2001</Ind>
      </Cterm>
    </Atom>

    <Atom>
      <Rel>keep</Rel>
      <Ind>Mary</Ind>
      <Var>object</Var>
    </Atom>
    
  </And>

</Consider>

Document 1' -- Universally Closed Clauses of 'And' in 'Consider' Wrapper (Document 1 After 'closure' Propagation):

<Consider>

  <And>

    <Implies closure="universal">
      <And>
        <Atom>
          <Rel>buy</Rel>
          <Var>person</Var>
          <Var>merchant</Var>
          <Var>object</Var>
        </Atom>
        <Atom>
          <Rel>keep</Rel>
          <Var>person</Var>
          <Var>object</Var>
        </Atom>
      </And>
      <Atom>
        <Rel>own</Rel>
        <Var>person</Var>
        <Var>object</Var>
      </Atom>
    </Implies>
    
    <Atom closure="universal">
      <Rel>buy</Rel>
      <Ind>Mary</Ind>
      <Ind>John</Ind>
      <Cterm>
        <Ctor>book</Ctor>
        <Ind>Elliotte Rusty Harold</Ind>
        <Ind>XML Bible</Ind>
        <Ind>2001</Ind>
      </Cterm>
    </Atom>

    <Atom closure="universal">
      <Rel>keep</Rel>
      <Ind>Mary</Ind>
      <Var>object</Var>
    </Atom>
    
  </And>

</Consider>

14. Appendix 2: 'own' Example as Universal 'Assert' with Existential Query

Document 2a -- Universally Closed 'And' Elements in 'Assert' Wrapper:

<Assert>

  <And innerclose="universal">
  
    ... content from Appendix 1, Document 1 ...
    
  </And>

</Assert>

Document 2b -- Existentially Closed Atom in 'Query' Wrapper (Response Provable from 'Assert'):

<Query>

  <Atom closure="existential">
    <Rel>own</Rel>
    <Var>person</Var>
    <Var>object</Var>
  </Atom>

</Query>

15. Appendix 3: 'own' Example as Universal Query

Document 3 -- Universally Closed 'And' Elements in 'Query' Wrapper (No 'Assert' Given for Proving Response):

<Query>

  <And innerclose="universal">
  
    ... content from Appendix 1, Document 1 ...
    
  </And>

</Query>

16. Issues List

1. 2004-06-21 Q (Michael Sintek): Should "pragmatic" top-level rulebase elements like 'Rule', 'Fact', 'Query', 'Ic' (integrity constraint), etc. be used instead of the top-level connectives (keeping only the corresponding sublevel connectives)? A (Harold Boley): While 'Rule' and 'Fact' elements could be combined into an axiomatic 'Assertion' element, 'Query' will be removed from 'Rulebase' anyway (instead becoming the second element of a 'Turnstile', whose first element is the 'Rulebase'), and 'Ic' will likely be introduced outside of 'Rulebase' as well; however, the remaining 'Assertion' element would lead to a deeper markup, which would be a problem especially for all earlier Horn-like sublanguages (alternating speech-act-like "pragmatic" wrapper information with "semantic" content information also is a problem, and an interesting follow-up issue for Reaction Rules).
   2004-09-12: Solved via existing 'Query' element and new 'Assert' element.
   
   
2. 2004-09-07 Q (Ian Horrocks, Peter Patel-Schneider): Can the distinction between to-be-asserted vs. to-be-checked formulas be moved out of the logic language? A (Harold Boley, Mike Dean): Yes, makes sense.
   2004-09-12: Solved by strict separation of declarative content from procedural performatives.
   
   
3. 2004-09-14 Q (Benjamin Grosof): Besides the delivery of derived facts (via 'Assert'), also bindings should be allowed on the top level (cf. answerset in current SweetRules effort); how would this fit into the picture? A (Harold Boley): Could be introduced as an 'in-reply-to'-like 'Response' performative (complementary to 'Query'); however, content language would need to encode variable bindings, which are less 'logical' than formulas.
   2004-09-14: Factor out here, but work on it as part of surrounding shells of (interactive/reactive) RuleML and SWSI sublanguages.
   
   
4. 2004-09-14 Q (Mike Dean): What relationships exist with the W3C DAWG query effort? A (Harold Boley, Benjamin Grosof): While using different query notions, collaboration with DAWG should be increased, e.g. offering them our retrieval-query use cases; this requires that we can mark up query content with our preliminary 'Query' element (the Introduction elaborates our envisaged collaborations).
   2004-09-19: Solved by normatively restricting new Syntax and Semantics section to content language.
   
   
5. 2004-09-21 Q (Mike Dean): Could we introduce a ("universal") default value for the 'closure' and 'innerclose' attributes? A (Harold Boley, Ian Horrocks): Looks worth checking.
   2004-09-23: Since we can also have explicit ('Exists') quantifiers over formulas, formulas generally -- e.g., in the scope of quantifiers -- cannot have a global DTD/XSD default (a syntactic default would also interfer with the 'innerclose' propagation now elaborated in Syntax and Semantics).
   
   
6. 2004-09-21 Q (Ian Horrocks, Mike Dean): How can we further clarify that 'Query' and 'Assert' are only illustrations of how others could use FOL RuleML content in their performatives? A (Harold Boley, Ian Horrocks): Let's introduce a neutral performative for FOL formulas agnostic w.r.t. them being asserted, queried, or whatever.
   2004-09-25: Solved by the introduction of 'Consider' performative as non-normative wrapper in Syntax and Semantics and its color-wrapped illustration in new Appendix 1.
   
   
7. 2004-09-27 Q (Michael Kifer): What is the use of the 'innerclose' attribute, in contrast to the 'closure' attribute? A (Harold Boley): 'innerclose' marks up the convention of clausal theorem provers to close off all elements in a set of clauses, each with their own scope, while 'closure' closes off a single clause, establishing its scope.
   2004-09-27: Clarified in the "In the spirit of the logic ..." paragraph of the Introduction.
   
   
8. 2004-09-28 Q (Benjamin Grosof): Could it be indicated that the 'innerclose' attribute is more experimental than the 'closure' attribute? A (Harold Boley, Mike Dean): Yes: 'innerclose' has recently been introduced on top of 'closure'.
   2004-09-28: Solved by a role comparison of both attributes in the paragraph after the DTD in Syntax and Semantics, with reference to a new Document 1' in Appendix 1.
   
   
9. 2004-10-26 Q (Pat Hayes): Can we rename 'Neg' into 'Not', because this is the standard word to refer to classical negation (cf. Peter Patel-Schneider's Comments)? A (Harold Boley): Let's think more about it, keeping compatibility with negation-as-failure communities in mind, some of which would rename 'Naf' into 'Not'.
   2004-11-02: Still Open Issue after the 2004-10-28 RuleML telecon, Benjamin Grosof's markup tagnames for negation, and another JC telecon; therefore either keep 'Neg' or rename it into 'Not' according to the feedback obtained after Mike Dean's SWRL FOL announcement.

Acknowledgments

This document was produced as part of the DARPA DAML Program, and has benefited from extensive discussion in the Joint US/EU ad hoc Agent Markup Language Committee, with contributions from Sandro Hawke and Pat Hayes being worthy of particular mention. It has also benefited from the close cooperation of the RuleML initiative, and input from the Semantic Web Services Initiative (SWSI).