W3C

RIF Core Design

W3C Editor's Draft @@not-published

This version:
@@not-published
Latest version:
Previous version:
Editors:
Harold Boley
Michael Kifer

Abstract

This document, developed by the Rule Interchange Format (RIF) Working Group, specifies the core design for a format that allows rules to be translated between rule languages and thus transferred between rule systems.

In Phase 1, the RIF Working Group is first defining a Core Condition Language. This condition language is envisioned to be a shared part of all RIF dialects. As a first step, it is used in this document to define rule bodies of the RIF Core Horn Language. A human-oriented syntax, an XML syntax, and the semantics of the condition language and of the Horn rule language are given.

Status of this Document

May Be Superseded

This section describes the status of this document at the time of its publication. Other documents may supersede this document. A list of current W3C publications and the latest revision of this technical report can be found in the W3C technical reports index at http://www.w3.org/TR/.

Please Comment By @@no-due-date

Send comments to public-rif-wg@w3.org (assuming you're in the WG)

No Endorsement

Publication as a Working Draft does not imply endorsement by the W3C Membership. This is a draft document and may be updated, replaced or obsoleted by other documents at any time. It is inappropriate to cite this document as other than work in progress.

Patents

This document was produced under the 5 February 2004 W3C Patent Policy. The Working Group maintains a public list of patent disclosures relevant to this document; that page also includes instructions for disclosing [and excluding] a patent. An individual who has actual knowledge of a patent which the individual believes contains Essential Claim(s) with respect to this specification should disclose the information in accordance with section 6 of the W3C Patent Policy.


Table of Contents

1. RIF Overview

(Editor's Note: This text is maintained on wiki page RIF Overview).

Based on the RIF Use Cases and Requirements, this document develops the RIF Core through a set of foundational concepts shared by all RIF dialects. The overall RIF design takes the form of a layered architecture organized around the notion of a dialect.

A dialect is a rule-based language with a well-defined syntax and semantics. This semantics must be model-theoretic, proof-theoretic, or operational in this order of preference. Some dialects might be proper extensions of others (both syntactically and semantically) and some may have incompatible expressive power. However, all dialects are required to extend the RIF Core dialect.

  • *** Issue(MK): The above says that a dialect is a rule-based language, and RIF is about rules. But we also had a requirement(??) to support full FOL ***

From a theoretical perspective, RIF Core corresponds to the language of definite Horn rules (see [Horn Logic]) with equality (and with a standard first-order semantics). Syntactically, however, RIF Core has a number of extensions to support features such as objects and frames, URIs as identifiers for concepts (so-called Webization), and primitive data types. The semantics also has provisions for future extensions towards dialects that support pure FOL, dialects that support negation as failure (NAF), business (or production) rules, reactive rules, and other features.

Eventually, it is hoped that RIF dialects will cover a number of important paradigms in rule-based specification and programming. Our main target paradigms include production rules, logic programming, FOL-based rules, reactive rules, and normative rules (integrity constraints).

The central part of RIF Core is its Condition Language. The condition language defines the syntax and semantics for the bodies of the rules in the core of RIF and the syntax for the queries. However, it is hoped that the condition language will have wider applicability in RIF. In particular, it might be reusable as a sublanguage for specifying the conditional part of the bodies in production rules, reactive rules, and in normative rules.

  • *** Comment: Condition Language is currently a working title. I cringe at the word Webization. A better term? ***

As mentioned, webization of RIF means that URI constants can serve both as logical constants and as names of predicate and function symbols. This is not normally allowed in first-order logic, but is common practice in Logic Programming (e.g., [Prolog], [F-logic], [HiLog]) and in [RDF]. Nevertheless, RIF Core supports Webization while remaining completely within the realm of the first order semantics. This is achieved by building RIF on the basis of a multisorted first-order logic, which permits symbols to be polymorphic, i.e., to have more than one sort. A symbol can simultaneously have a primitive sort (for instance, a string), an arrow sort (which permits the symbol to appear in the role of a function symbol), and a Boolean sort (which enables that symbol to play the role of a predicate symbol). In this setting, URIs are constants in just one of the primitive sorts of RIF. Integers, strings, dates, time, and others are treated as other primitive sorts. Thus, the single mechanism of a polymorphic multisorted logic accounts both for Webization and also enables RIF to support primitive data types of [XML Schema] as well as other possible types. This also simplifies the relationship with RDF and makes higher-order dialects based on [HiLog] and [Common Logic] possible.

RIF Core is described in the current document by means of the following:

  1. A MOF/UML metamodel (abstract syntax)

  2. A BNF syntax (concrete human-oriented syntax, for illustration/explanation purposes only)

  3. An XML syntax (concrete serialization syntax, for illustration purposes only)

  4. A model-theoretic semantics

The BNF and XML syntaxes are derived from the abstract syntax. The model-theoretic semantics is designed for modularity and to enable further extensions.

The current document is a first draft of the RIF Core specification. A number of extensions are planned to support frame-based syntax, built-ins, additional primitive XML data types, the notions of compliance with RIF, and so on. Tool support for RIF Core is forthcoming. Additional RIF dialects, which extend the core, will be specified in other documents byu this working group.

2. RIF Condition Language

(Editor's Note: This text is maintained on wiki page RIF Condition Language).

The RIF Condition Language is intended to be a common basis for several dialects of RIF. First of all, it is used by RIF Core, as described in this document. The other future dialects or groups of dialects where the condition language or its extensions might be used include:

  • Rule bodies and queries in declarative logic programming dialects (LP)

  • Rule bodies in first-order dialects (FO)

  • Conditions in the rule bodies of production rule dialects (PR)

  • The event and condition parts of the rule bodies in reactive rules dialects (RR)

  • Integrity constraints (IC)

It should be noted, however, that apart from RIF Core no decision has been made regarding which dialects will ultimately be part of RIF.

The RIF condition language is intended to be used only in rule bodies and queries, not in rule heads. The various RIF dialects diverge in the way they specify, interpret, or use rule heads and other components of the rules. By focusing on the condition part of the rule bodies we achieve maximum syntactic and a great deal of semantic reuse among the dialects. This document describes Positive Conditions.

  • ***Comment (MK): The following paragraph should be elsewhere. Their place should be determined after we decide where to put section A.6 referenced below. Or maybe in RIFRAF. ***

Since different semantics are possible for syntactically identical rule sets, the semantics of RIF rule sets is specified by a predefined attribute. We elaborate on this proposal in Section A.6 Semantics. The idea is to organize the most important known semantic and syntactic features into a taxonomy (which could be extended to accommodate new semantics and syntax), and the values of the aforementioned attribute would come from that taxonomy.

2.1. Positive Conditions

(Editor's Note: This text is maintained on wiki page Positive Conditions).

The language of positive RIF conditions determines what can appear as a body (the if-part) of a rule supported by RIF Core. As explained in Section [[Overview]], RIF Core corresponds to definite Horn rules, and the bodies of such rules are conjunctions of atomic formulas without negation. However, it is well-known that disjunctions of such conditions can also be used in the bodies of rules without changing the essential properties of the rule language. This is based on the fundamental logical tautology (h ← b ∨ c) ≡ ((h ← b) ∧ (h ← c)). In other words, a rule with a disjunction in the body can be split into two or more rules that have no such disjunction.

In a later draft, positive RIF conditions will be extended to include builtins. Although there was no decision regarding concrete extensions beyond Horn rules, the intent behind this condition language is that it will be shared among the bodies of the rules expressed in the envisioned RIF dialects LP, FO, PR, RR, and can also be used to uniformly express integrity constraints (IC) and queries.

This section presents a syntax and semantics for the RIF condition language, which supports primitive data types (such as integer, string, decimal, time, dateTime), and the use of URIs to refer to constants, predicates, and functions -- an essential ingredient in making RIF dialects suitable as Web languages.

To support Webizing and the future higher-order dialects based on HiLog and Common Logic, the RIF Core language does not separate symbols used to denote constants from symbols used as names for functions or predicates. Instead, all symbols are drawn from the same universal set. When desired, separation between the different kinds of symbols is achieved through the mechanism of sorts. In logic, the mechanism of sorts is used to classify symbols into separate groups. Currently RIF Core supports the sort uri for URIs, and the sorts integer (http://www.w3.org/TR/2004/REC-xmlschema-2-20041028/datatypes.html#integer, decimal (http://www.w3.org/TR/2004/REC-xmlschema-2-20041028/datatypes.html#decimal), time (http://www.w3.org/TR/2004/REC-xmlschema-2-20041028/datatypes.html#time, string (http://www.w3.org/TR/2004/REC-xmlschema-2-20041028/datatypes.html#string), and dateTime (http://www.w3.org/TR/2004/REC-xmlschema-2-20041028/datatypes.html#dateTime). Other sorts (such as long, double, duration and date) will be added in future drafts.

To support the Webizing and enable extensibility, the underlying logic of RIF is not only multi-sorted (i.e., allows multiple sorts), but it also allows symbols to be polymorphic (i.e., the same symbol is allowed to have several sorts). Some sorts can be disjoint (for example, integer and dateTime) and others not (for example, uri should probably be defined as a subsort of the sort string). RIF dialects will be able to decide which sorts will be allowed for predicate symbols, which for function symbols, and so on. For example, we might decide that only strings (which includes URIs, if uri is a subsort of string) can be used for predicate names. Or we can decide that only uri and local (where local could be some subsort of string) are allowed for predicates and functions.

  • *** Rewrite the above when we decide the above issues. ***

For didactic reasons, we start with a single sort, which includes all constants, function symbols, and predicate names. The multisorted RIF logic is described in Section Multisorted RIF Logic.

METAMODEL

A MOF/UML metamodel is a schema-level device for specifying an object-oriented

abstract syntax consisting of syntactic classes with ('isa') generalizations as well as multiplicity- and role-labeled ('partof') associations. The classes are partitioned into classes that will not be visible in serializations (written in all-uppercase letters) and classes that will be visible in instance markup (written with a leading uppercase letter only).

The central class of RIF, CONDITION, is specified recursively through its subclasses and their parts. Three pairs of roles distinguish between the declare and formula parts of the Exists class, the left-hand side (lhs) and right-hand side (rhs) of the Equal class, and the operation (op) and arguments (arg) of the Uniterm class, where multiple arguments are subject to an ordered constraint (the natural "left-to-right" order):

The classes Var, CONDITION, and POSITIVE will be required in the metamodel of Horn Rules.

SYNTAX

The metamodel of Section [METAMODEL] can be instantiated to a concrete syntax via a (stripe-skipping) mapping from role-labeled components ('subparts') to position-identified syntax. To exemplify the recursive transformation, we use the MOF/UML class Equal with its two roles lhs and rhs leading to TERM class occurrences. Employing a slotted notation Sourceclass(..., role->Targetclass, ...), Equal can be mapped to a role-skipped version, where positional information replaces explicit roles as follows:

  1. Equal( rhs->TERM2, lhs->TERM1 )

  2. Equal( lhs->TERM1, rhs->TERM2 )

  3. Equal( 1->TERM1, 2->TERM2 )

  4. Equal( TERM1, TERM2 )

  5. TERM1 = TERM2

*** Comment: wiki-tr version currently doesn't show underlines.

The first step (from 1. to 2.) fixes an order for roles (here, "left-hand/right-hand side" order), and is omitted if the roles are already given in that order (as in the diagram of the above model). The intermediate version 3. replaces the roles with natural numbers, to prepare the transition from roles to positions, and performs the recursive transformation (indicated by underlines) of the TERM classes. The prefinal version 4. just uses TERM1 and TERM2 themselves in their argument positions of the Equal nonterminal (the roles thus became skipped). The final version 5. is specific to the Equal nonterminal, which is distinguished by writing it as the equality operator, =, in the infix notation.

The resulting BNF syntax below is used throughout this document to explain and illustrate the main ideas. This syntax is similar in style to what in OWL is called the Abstract Syntax http://www.w3.org/TR/owl-semantics/syntax.html.

  CONDITION   ::= CONJUNCTION | DISJUNCTION | EXISTENTIAL | POSITIVE
  CONJUNCTION ::= 'And' '(' CONDITION* ')'
  DISJUNCTION ::= 'Or' '(' CONDITION* ')'
  EXISTENTIAL ::= 'Exists' Var+ '(' CONDITION ')'
  POSITIVE    ::= Uniterm | Equal
  Uniterm     ::= Const '(' TERM* ')'
  Equal       ::= TERM '=' TERM
  TERM        ::= Const | Var | Uniterm
  Const       ::= CONSTNAME | '_'SORTNAME'"'CONSTNAME'"'
  Var         ::= '?' | '?'VARNAME | '_'SORTNAME'?' | '_'SORTNAME'?'VARNAME

The above is a standard syntax for a variant of first-order logic. The application of a symbol from Const to a sequence of terms is called Uniterm ("Universal term") since it can be used to play the role of a function term or an atomic formula depending on the syntactic context in which the application occurs. The non-terminal POSITIVE stands for positive literal formula, which can later be complemented with "negated literal formula". EXISTENTIAL stands for "existential formula", which in Horn-like conditions is the only quantified formula but in later conditions may be complemented with "universal formula" (Var+ denotes the list of free variables in CONDITION). The production CONJUNCTION defines conjunctions of conditions, and DISJUNCTION denotes disjunctions. Finally, CONDITION assembles everything into what we call RIF conditions. RIF dialects will extend these conditions in various ways.

  • *** The BNF syntax will need to be fixed. Possibly with infix And and Or. The problem currently is that And and Or are function predicates with special meaning, which is not good for interchange. BNF in this way also does not correspond to UML and XML where conjunction/disjunction are not function symbols but connectives. This also forces us to make exceptions for And and Or. ***

Since initially we focus on an unsorted RIF language, constants, function symbols, and predicate names all belong to the same set of symbols (Const). Variables are also unsorted, i.e., they range over the entire domain. Sorts are introduced in Section [Multisorted RIF Logic]. However, in preparation of the multisorted version, the above BNF syntax already introduces SORTNAME-enriched choices for Const and Var that will be required in the [Multisorted RIF Logic].

*** Currently CONSTNAME is undefined. In WD2 sorts should be dealt with right from the start and then constants can all have the syntax _sortname"..." with abbreviated syntax for strings, integers, and decimals. ***

The above BNF, where TERM* is understood as TERM* ::= | TERM TERM*, uses spaces to indicate Lisp-like whitespace (SPACE, TAB, or NEWLINE) character sequences in the defined language; these must consist of at least one whitespace character when used as the separator between adjacent TERMs, and can consist of zero or more whitespace characters elsewhere. Where spaces are omitted from the BNF, as between '?' and VARNAME in '?'VARNAME, there must be no whitespace character in the defined language.

At this point we do not commit to any particular vocabulary for the names of constants, variables, or sorts. For the moment, NamedElement in the UML model can be either CONSTNAME, or VARNAME, or SORTNAME. These are still assumed to be alphanumeric character sequences (except 'And' and 'Or'). For more details on this see [Multisorted RIF Logic].

  • *** Issue: Should we allow certain special characters, so generalize "any alphanumeric character sequence (except 'And' and 'Or')" to, e.g., "any character sequence (except 'And' and 'Or') not containing special characters of the defined language except '_' (hence '?', '"', '=', parentheses, and whitespace are prohibited)"? ***

A stand-alone symbol '?' denotes an anonymous variable; each occurrence of an anonymous variable represents a completely new variable that does not occur elsewhere in the same formula.

  • *** Issue: Jos raised the issue of whether disjunctions should be allowed in the core spec. ***

    *** Issue: Jos and Adrian asked whether it is useful to have anonymous variables. MK: Indeed, these variables are not needed in the rules, but in queries they indicate when answers for some variables are not required. In fact, we might even need "silent" variables, which can repeat, but are not returned as answers. In prolog these are named variables that start with an underscore. So, silent and anonymous variables are interface issues, not semantics. HB: If we keep anonymous variables, then we need to introduce NAMEDVAR/ANONVAR non-terminals and restrict Exists' Var+ to NAMEDVAR+; same for Forall's Var+ in Horn Rules ***

Note that variables in the RIF Condition Language can be free and quantified. All quantification is explicit. All variables introduced by quantification should also occur in the quantified formula. Initially, only existential quantification is used. Universal quantification will be introduced later. We adopt the usual scoping rules for quantifiers from first-order logic. Variables that are not explicitly quantified are free.

Free variables arise because CONDITION can occur in an if part of a rule. When this happens, the free variables in a condition formula are precisely those variables that also occur in the then part of the rule. We shall see in Section Horn Rules that such variables are quantified universally outside of the rule, and the scope of such quantification is the entire rule. For instance, the variable ?Y in the first RIF condition of Example 1 is quantified, existentially, but ?X is free. However, when this condition occurs in the if part of the second rule in Example 1, then this variable is quantified universally outside of the rule. (The precise syntax for RIF rules will be given in Section Horn Rules.)

Example 1 (A RIF condition in and outside of a rule)

 RIF condition:
                        Exists ?Y (condition(?X ?Y)) 

 RIF Horn rule:
        Forall ?X (then(?X) :-  Exists ?Y (condition(?X ?Y)))

When conditions are used as queries, their free variables are used to carry answer bindings back to the caller.

The following is a possible XML-serializing mapping of the MOF/UML metamodel in Section [METAMODEL] (and of the above BNF syntax). This XML serialization is partially stripe-skipped in that it uses positional information instead of most role elements. The only place where role elements ('declare' and 'formula') are explicit is within the Exists element. Following the examples of Java and RDF, we use capitalized names for class elements and names that start with lowercase for role elements. To exemplify, the above BNF mapping of the MOF/UML class Equal can be modified to an XML mapping by using a new last step as follows:

  1. Equal( TERM1, TERM2 )

  2. <Equal> TERM1 TERM2 </Equal>

The all-uppercase non-terminals in BNF, such as CONDITION, become XML entities. They act like macros and are not visible in instance markup. The other non-terminals and symbols (such as Exists or =) become XML elements, as shown below.

- And     (conjunction)
- Or      (disjunction)
- Exists  (quantified formula for 'Exists', containing declare and formula roles)
- declare (declare role, containing a Var)
- formula (formula role, containing a CONDITION formula)
- Uniterm (atomic or function-expression formula)
- Equal   (prefix version of term equation '=')
- Const   (individual, function, or relation constant)
- Var     (logic variable, empty for anonymous variable)

A DTD for RIF Horn rules is discussed in Appendix RIF Validation. An XML Schema is under development.

The following example illustrates XML serialization of RIF conditions.

Example 2 (A RIF condition and its XML serialization):

a. RIF condition:

  And ( Exists ?Buyer (purchase(?Buyer ?Seller book(?Author LeRif) $49)) ?Seller=?Author )

b. XML serialization:

  <And>
    <Exists>
      <declare><Var>Buyer</Var></declare>
      <formula>
        <Uniterm>
          <Const>purchase</Const>
          <Var>Buyer</Var>
          <Var>Seller</Var>
          <Uniterm>
            <Const>book</Const>
            <Var>Author</Var>
            <Const>LeRif</Const>
          </Uniterm>
          <Const>$49</Const>
        </Uniterm>
      </formula>
    </Exists>
    <Equal>
      <Var>Seller</Var>
      <Var>Author</Var>
    </Equal>
  </And>

SEMANTIC STRUCTURES (a.k.a. INTERPRETATIONS)

The first step in defining a model-theoretic semantics for a logic-based language is to define the notion of a semantic structure, also known as an interpretation.

  • There are several equivalent ways to define first-order semantic structures. The one we adopt has the advantage that it generalizes to rule sets with negation as failure (NAF) and to logics for dealing with uncertainty and inconsistency. The difficulty is that some popular theories for NAF, such as the well-founded semantics, are based on three-valued semantic structures. Some popular ways to handle uncertain or inconsistent information (which is certainly important in the Web environment) rely on four-valued and other multi-valued logics. Therefore, following M. Fitting, Fixpoint Semantics for Logic Programming A Survey, Theoretical Computer Science, 1999, we build our definitions to be compatible with future RIF dialects, which will be based multivalued logics.

A semantic structure, I, is a tuple of the form <D,IC, IV, IF, IR>, which determines the truth value of every formula, as explained below. Currently, by formula we mean anything produced by the CONDITION production in the BNF. Later on this term will also include rules. Other dialects might extend this notion even further.

The set of truth values is denoted by TV. For RIF Core, TV includes only two values, t (true) and f (false).

  • Some RIF dialects will have additional truth values. For instance, some versions of NAF use three truth values: t, f, and u (undefined). Handling of contradictions and uncertainty requires at least four truth values: t, u, f, and i (inconsistent).

The set TV has a total or partial order, called the truth order; it is denoted with <t. In RIF Core, f <t t, and it is a total order.

  • In the well-founded semantics for NAF, f <t u <t t, and it is again a total order. But in four-valued logics, which are often used for dealing with uncertain or inconsistent information, the truth order is partial: f <t u <t t and f <t i <t t. Such logics also have another partial order, called the knowledge order <k: u <k t <k i; and u <k f <k i. Under the knowledge order, true and false are incomparable, and facts that are both true and false receive the truth value i, which is the least upper bound of f and t in the knowledge order.

To define how semantic structures determine the truth values of RIF formulas, we introduce the following sets:

  • D - a non-empty set of elements called the domain of I,

  • Const - the set of constants, predicate names, and function symbols,

  • Var - the set of variables.

As mentioned above, an interpretation, I, consists of a domain, D, and four mappings:

  • IC from Const to elements of D

  • IV from Var to elements of D

  • IF from Const to functions from D* into D (here D* is a set of all tuples of any length over the domain D)

  • IR from Const to truth-valued mappings D* -> TV

Using these mappings, we can define a more general mapping, I, as follows:

  • I(k) = IC(k) if k is a constant in Const

  • I(?v) = IV(?v) if ?v is a variable in Var

  • I(f(t1 ... tn)) = IF(f)(I(t1),...,I(tn))

Truth values for formulas in RIF Core are determined using the following function, denoted ITV:

  • Atomic formulas: ITV(r(t1 ... tn)) = IR(r)(I(t1),...,I(tn))

  • Equality: ITV(t1=t2) = t iff I(t1) = I(t2); ITV(t1=t2) = f otherwise.

  • Conjunction: ITV(And(c1 ... cn)) = mint(ITV(c1),...,ITV(cn)), where mint is minimum with respect to the truth order.

  • Disjunction: ITV(Or(c1 ... cn)) = maxt(ITV(c1),...,ITV(cn)), where maxt is maximum with respect to the truth order.

  • Quantification: ITV(Exists ?v1 ... ?vn (c)) = maxt(I*TV(c)), where maxt is taken over all interpretations I* of the form <D,IC, I*V, IF, IR>, where I*V is the same as IV except possibly on the variables ?v1,...,?vn (i.e., I* agrees with I everywhere except possibly in its interpretation of the variables ?v1 ... ?vn).

Notice that the mapping ITV is uniquely determined by the four mapping comprising I and, therefore, it does not need to be listed explicitly.

Multisorted RIF Logic

RIF uses multi-sorted logic to account for primitive data types, the use of URIs as identifiers for objects and concepts, and more. This framework is general enough to accommodate a number of popular extensions, such as Prolog, HiLog, F-logic, Common Logic, and RDF, which allow the same symbol to play multiple roles. For instance, the same symbol, foo, can be used as a constant, a predicate of several different arities, and as a function symbol of different arities.

In a multisorted RIF Core, each constant from Const is associated with one or more sorts. A sort can be primitive, an arrow sort, or a Boolean sort. Arrow sorts are also known as function sorts, and Boolean sorts are also known as predicate sorts. Collectively they are also known as signatures of predicate and functions symbols.

Primitive sorts are drawn from a fixed collection of sorts PS1, ..., PSn. These sorts are intended to model primitive data types. For instance, RIF Core supports the sorts integer, string, dateTime, and uri among others. The same constant can be associated with more than one primitive sort. It is also possible that one sort would be a subsort of another. For example, the sort of short integers might be defined as a subsort of the sort of long integers, so every constant of the sort short would also be associated with the sort long. In RIF, constants of different sorts are distinguished syntactically. A concrete syntax for sorted constants and variables is shown in Section [[Syntax for Primitive Sorts]].

The language of the RIF sorted logic also provides a special sublanguage for defining the sorts of function symbols and predicates. An arrow sort is a statement of the form s1 × ... × sk → s, where s1, ..., sk, s are names of primitive sorts (i.e., one of the PS1, ..., PSn). For instance, dateTime × integer → dateTime could be an arrow sort for a function. A Boolean sort is a statement of the form <s1 × ... × sk>, where, again, s1, ..., sk are names of primitive sorts. For instance, the predicate HappenedBefore may have a Boolean sort <dateTime × dateTime>. The arrow and Boolean sorts, along with the primitive sorts, are used in the definition of well-formed terms and formulas. This notion is defined in Section [Formalization of the Multisorted RIF].

  • Recall that RIF Core uses the symbols from Const to denote constants, predicates, and function symbols alike, so the same symbol can occur in multiple contexts. However, sometimes it is useful to restrict the contexts in which various symbols are allowed to occur. For instance, Prolog or RDF don't place any such restrictions, but OWL-DL has a unique role for each symbol. This restriction of the context is accomplished by controlling the sorts that are associated with each constant. For instance, if we do not want integers to occur as predicate and function symbols then we will not associate any arrow or Boolean sorts with the constants that are associated with the primitive sort integer. On the other hand, we do want URIs to denote concepts and other predicates. In that case, we would associate every Boolean sort with every constant that has a primitive sort URI. If we want to also allow local names for concepts and other predicates, then we might introduce a separate primitive sort, local, and allow the symbols that belong to this sort to have Boolean types.

RIF multisorted logic can also easily represent the syntax of the usual first order predicate calculus. To this end, we just need to ensure that each symbol in Const has exactly one sort associated with it. It could be a primitive sort, an arrow sort, or a Boolean sort, but it must be exactly one. In this case, any given symbol can occur either as a constant, or as a function symbol of one particular arity, or as a predicate of one particular arity.

Formalization of the Multisorted RIF Logic

In addition to the syntax for the sorted literals, RIF Core needs the following extensions. First, we introduce the following new functions:

  • PSort: Const → powerset(Primitive_Sorts)

  • ASort: Const → powerset(Arrow_Sorts)

  • BSort: Const → powerset(Boolean_Sorts)

Each of these functions associates a (possibly empty) set of sorts (primitive, arrow, or Boolean) with every constant c ∈ Const.

PSort is also defined on variables:

  • PSort: Var → powerset(Primitive_Sorts)

The intended meaning is that if ?v ∈ Var and PSort(?v) = {s1, ..., sk} then ?v can be bound only to function terms that simultaneously belong to sorts s1, ..., sk (we define what it means for a function term to belong to a primitive sort below). If PSort(?v) is an empty set, then ?v is an unsorted variable, which ranges over the entire domain disregarding the boundaries among the sorts.

Well-formed function terms. Any constant, c ∈ Const, is a well-formed function term of sort s, for any s ∈ PSort(c).

Note that this means that the same constant can be a well-formed term of several different sorts because we allow several primitive sorts to be associated with the same constant. The informal meaning is that the term belongs to the "intersection" of all the sorts with which it is associated.

By induction, if f(t,,1,, ... t,,k,,) is a function term then it is a well-formed function term of sort s if there is an arrow sort s,,1,,, ..., s,,k,, &rarr; s &isin; ASort(f) such that t,,1,,, ..., t,,k,, are well-formed function terms of sorts s,,1,,, ..., s,,k,,, respectively.

It is convenient to extend the mapping PSort from constants to function terms as follows:

  • PSort(t) = { s | t is a well-formed term of sort s }

Well-formed atomic formula. We can now say that an atomic formula p(t,,1,,, ..., t,,k,,) is well-formed if and only if `t1, ..., tk are well-formed function terms and there is a Boolean sort s1 × ... × sk BSort(p) such that s1 ∈` PSort(t,,1,,), ..., s,,k,, &isin; PSort(t,,k,,).

From now on, we also require that all atomic formulas that occur in RIF conditions and rules must be well-formed.

Multisorted Syntax

Now we define how exactly the sorts are specified in RIF, i.e., how the functions PSort, ASort, and BSort are defined in practice.

Syntax for Primitive Sorts

In this document we will use the following syntax to specify the primitive sorts, which lie in the range of the function PSort:

   _sortname"value"

For instance, _integer"123" is a constant that belongs to the primitive sort integer, _dateTime"2007-11-23T03:55:44-02:30" is a constant of sort dateTime, and _uri"ftp://example.com/foobar" is a constant that belongs to the sort uri. The part of such constants that occurs inside the double quotes is called a literal of the sorted constant. The surrounding double quotes are not part of the literal. If a double quote must be included as part of a literal, it must be escaped with the backslash. Some frequently used sorted literals, namely strings, integers, and decimals, will have alternative short notation, which is explained below.

Variables can also be sorted. A variable ?v of sort dateTime, for example, is represented as _dateTime?v. We will continue to use our old notation, ?v, for unsorted variables, i.e., variables that range over the entire domain, which includes all sorts.

  • Association of multiple sorts with the same constant can be achieved with the help of equality. For instance, an assertion _sort1"foo" = _sort2"foo" ensures that these two constants represent the same entity, which therefore must belong simultaneously to sorts sort1 and sort2. If we want URIs to be also treated as strings, we can assert an equality _uri"xyz" = _string"xyz" for every URI xyz. Or, more concisely, we could write FORALL ?x (_uri?x = _string?x).

The XML syntax for sorts can utilize the 'sortal' attribute associated with XML term elements such as Const. For instance, the earlier dateTime example can be represented as <Const sortal="dateTime">2007-11-23T03:55:44-02:30</Const>. A correspondingly sorted variable xyz would be written as <Var sortal="dateTime">xyz</Var>.

Many primitive sorts in RIF may be based on the XML Schema data types and thus it is expected that some names of RIF primitive types will be references to those XML Schema types. In this case, these sorts will have the form _uri"...".

In this version of the RIF Core document, we define the following primitive sorts:

  • integer. Constant symbols of this sort have the form _integer"XYZ" where XYZ is an integer value written in decimal notation. Example: _integer"123". Integers also have an alternative short notation, which does not require the _integer"..."` wrapper. Example: 123.

  • decimal. Constant symbols if this sort have the form _decimal"XYZ", where XYZ has the form of a number written in decimal notation with optional decimal point. Example: _decimal"123.45". Decimals also have an alternative short notation, which dosnt require the _decimal"..." wrapper. Example: 123.45.

  • string. Constants of this sort have the form _string"XYZ", where XYZ is any sequence of unicode characters. Example:

    • _string"a string". Double quotes that appear inside strings are escaped with a backslash. Strings have also an alternative short notation. Example: 'a string'. In this notation, single quotes that occur inside such strings are escaped with a backslash.

  • uri. Constants of this sort have the form _uri"XYZ" where XYZ has the form of a URI.

  • time. Constants of the form _time"HH:MM:SS.s", where HH is a number in the range of 0..11 and MM and SS are numbers in the range 0..59. The part .s is optional. It represents fractions of a second, where s is any positive integer. The symbols : and . are part of the syntax.

  • dateTime. This sort contains constants of the form _dateTime"SYYYY-NN-DDTHH:MM:SS.sZHH:MM", where YYYY represents the year with an optional minus sign S in front, NN represents a month in the range of 1..12, and DD represents the day of that month. The subsequent part HH:MM:SS.s represents time and is optional (see the description of time). The part that follows time, ZHH:MM represents the time zone. Here Z is a sign (+ or -), HH represents the difference in hours and MM in minutes.

The symbols -, :, and . are part of the syntax. dateTime is also allowed to have the form _dateTime"SYYYY-NN-DDTHH:MM:SS.sZ. Here the last Z is part of the syntax.

Other primitive sorts that are likely to be incorporated include long, double, date, and duration.

*** Comment (Axel): Need to define lexical space more precisely.***

Specifying Arrow and Boolean Sorts

Arrow sorts are declared as follows. Note that multiple sorts can be declared for the same symbol.

`

  • :- sort   NAME   s1 * ... * sns ,   r1 * ... * rk → r ,   ...

`

Boolean sorts are declared similarly:

`

  • :- sort   NAME   s1 * ... * sn ,   r1 * ... * rk ,   ...

`

Note that constant is a symbol from Const whose syntax was specified in Section [[Syntax for Primitive Sorts]]. In most cases functions and predicates are denoted by URIs, so such a constant will have syntax _uri"...". Sorts are also symbols. In many cases sorts will be XML Schema data types referred to by URIs, in which case they will also have the form _uri"...".

*** Comment (MK): Need to provide BNF and XML syntax for arrow/Boolean sorts here.

*** Comment (MK): Need to decide if sort symbols are also coming from Const.

*** Comment (MK): Probably will need to have some form of compact URIs (curies).

Semantics of the Multisorted RIF Core

The definition of RIF semantic structures needs only minor modifications. A multisorted semantic structure I, consists of a domain D = D,,s1,, &cup; ... &cup; D,,sn,,, and the same four mappings as before. Each D,,si,, is the domain of interpretation of the primitive sort s,,i,,. Only the mappings IC, IV, and IF require some changes. These changes are expressed as additional constraints as indicated below.

  • IC from Const to elements of D.

    • New constraint: If constant c has sort s then I,,C,,(c) &isin; D,,s,,.

  • IV from Var to elements of D.

    • New constraint: If ?v is a variable of sort s then IV(?v) &isin; D,,s,,.

  • IF from Const to functions from D* into D (here D* is a set of all tuples of any length over the domain D).

    • New constraint: If f has an arrow type s,,1,,&times; ...&times; s,,k,, &rarr; s &isin; ASort(f) then IF(f) must be a (possibly polymorphic) function of type D,,s1,, &times; ... &times; D,,sk,, &rarr; D,,s,,, i.e., if d,,1,, &isin; D,,s1,,, ..., d,,k,, &isin; D,,sk,, then IF(d,,1,,,...,d,,k,,) must be in D,,s,, (if the arguments are not in D,,s1,, &times; ... &times; D,,sk,, then the result does not need to be in D,,s,,, but IF(f) can have other types, which restrict its behavior).

  • IR from Const to truth-valued mappings D* -> TV.

Using these mappings, we can define a more general mapping, I, as follows:

  • I(k) = IC(k) if k is a constant in Const

  • I(?v) = IV(?v) if ?v is a variable in Var

  • I(f(t,,1,, ... t,,n,,)) = IF(f)(I(t,,1,,),...,I(t,,n,,)).

    • New constraint: Here f(t,,1,, ... t,,n,,) must be a well-formed term as defined earlier.

The definition of ITV stays the same.

3. RIF Rule Language

(Editor's Note: This text is maintained on wiki page RIF Rule Language).

This section develops a Core RIF Rule Language by extending the RIF Condition Language, where conditions become rule bodies. RIF Phase I covers only Horn Rules and a number of extensions that do not increase the expressive power of the language. The envisioned RIF dialects will extend the core rule language by generalizing the positive RIF conditions and by other means.

3.1. Horn Rules

(Editor's Note: This text is maintained on wiki page Horn Rules).

This section defines Horn rules for RIF Phase 1. The syntax and semantics incorporates RIF Positive Conditions defined in Section Positive Conditions.

METAMODEL

A MOF/UML metamodel extending the metamodel of Positive Conditions is used to specify the object-oriented (striped) abstract syntax.

The central class Forall of RIF clauses is specified through its parts, a variable (Var) declaration and an Implies or POSITIVE formula, where Implies distinguishes if-CONDITION from then-POSITIVE parts:

The classes Var, CONDITION, and POSITIVE were specified in the metamodel of Positive Conditions.

  • *** Issue: A Ruleset class could be easily added to contain zero or more Forall RIF clauses (currently unordered, but how to interchange Prolog's textually ordered clauses?) ***

SYNTAX

The metamodel of Section [METAMODEL] can again be instantiated to a concrete syntax via a (stripe-skipping) role-to-position mapping extending the mapping for Positive Conditions. We exemplify the recursive transformation using the MOF/UML class Implies with its two roles if and then leading, respectively, to CONDITION and POSITIVE class occurrences. Implies is mapped to a role-skipped version, where positional information replaces explicit roles as follows:

  1. Implies( if->CONDITION, then->POSITIVE )

  2. Implies( then->POSITIVE, if->CONDITION )

  3. Implies( 1->POSITIVE, 2->CONDITION )

  4. Implies( POSITIVE, CONDITION )

  5. POSITIVE :- CONDITION

The first step (from 1. to 2.) fixes an order for roles (here, "backward chaining" order) and is omitted if the roles are already given in that order. The intermediate version 3. replaces the roles with natural numbers, to prepare the transition from roles to positions, and performs the recursive transformation (indicated by underlines) of the POSITIVE and CONDITION classes. The prefinal version 4. just uses POSITIVE and CONDITION themselves in their argument positions of the ("backward"-)Implies connective (the roles thus became skipped). The final version 5. is specific to the Implies connective, which is distinguished by writing it as an :- operator in the usual infix syntax.

The resulting BNF syntax extends the BNF syntax for Positive Conditions by the following productions:

  CLAUSE   ::= 'Forall' Var* '(' Implies | POSITIVE  ')'
  Implies  ::= POSITIVE ':-' CONDITION

Var, POSITIVE, and CONDITION were defined as part of the syntax for positive conditions in Positive Conditions. The symbol :- denotes the implication connective used in rules. The statement POSITIVE :- CONDITION should be informally read as if CONDITION is true then POSITIVE is also true.

RIF deliberately avoids using the connective ← here because in some RIF dialects, such as LP and PR, the implication :- will have different meaning from the meaning of the first-order implication ←.

Rules are generated by the Implies production. Facts are generated by the POSITIVE production, and can be viewed as the then part of a rule with an empty if (or with true as the if part). Finally, the CLAUSE production generates a universally closed rule or fact.

Note also that, since CONDITION permits disjunction and existential quantification, the rules defined by the Implies production are more general than pure Horn rules. This extension was explained in the introduction to Section [Positive Conditions].

The document [http://www.w3.org/2005/rules/wg/wiki/UCR RIF Use Cases and Requirements] includes a use case "Negotiating eBusiness Contracts Across Rule Platforms", which discusses a business rule slightly modified here as follows:

If an item is perishable and it is delivered to John more than 10 days after the
scheduled delivery date then the item will be rejected by him.

In the BNF syntax used throughout this document, this rule can be written in one of these two equivalent ways:

Example 3 (A RIF rule in human-readable syntax)

a. Universal form:

  Forall ?item ?deliverydate ?scheduledate ?diffdate
      (
        reject(John ?item) :-
           And ( perishable(?item)
                 delivered(?item ?deliverydate John)
                 scheduled(?item ?scheduledate)
                 timediff(?diffdate ?deliverydate ?scheduledate)
                 greaterThan(?diffdate 10) )
      )

b. Universal-existential form:

  Forall ?item
      (
        reject(John ?item) :-
           Exists ?deliverydate ?scheduledate ?diffdate
               (
                 And ( perishable(?item)
                       delivered(?item ?deliverydate John)
                       scheduled(?item ?scheduledate)
                       timediff(?diffdate ?deliverydate ?scheduledate)
                       greaterThan(?diffdate 10) )
               )
      )

In form (a), all variables are quantified universally outside of the rule. In form (b), the variables that do not appear in the rule then part are instead quantified existentially in the if part. It is well-known that these two forms are logically equivalent.

The following extends the mapping in Positive Conditions, which serializes the MOF/UML metamodel (and the BNF syntax) of RIF Core in XML. The Forall element contains the role elements declare and formula, which were earlier used within the Exists element of Positive Conditions. The Implies element contains the role elements then and if to designate these two parts of a rule. With this, the order between the then and the if parts of a rule becomes immaterial. To exemplify, the above BNF mapping of the MOF/UML class Implies can be modified to an XML mapping retaining the roles as follows:

  1. Implies( if->CONDITION, then->POSITIVE )

  2. Implies( then->POSITIVE, if->CONDITION )

  3. <Implies> <then> POSITIVE </then> <if> CONDITION </if> </Implies>

The first step again fixes an order for roles, but would not be needed since the roles will be retained.

- Forall  (quantified CLAUSE formula with 'Forall')
- Implies (implication, containing then and if roles in any order)
- then    (consequent role, containing POSITIVE)
- if      (antecedent role, containing CONDITION)

A DTD for this XML serialization is described in Appendix RIF Validation. Work is underway to define the structure of the rules in an XML Schema.

For instance, the rule in Example 3a can be serialized in XML as shown below.

Example 4 (A RIF rule in XML syntax)

<Forall>
  <declare><Var>item</Var></declare>
  <declare><Var>deliverydate</Var></declare>
  <declare><Var>scheduledate</Var></declare>
  <declare><Var>diffdate</Var></declare>
  <formula>
    <Implies>
      <then>
        <Uniterm>
          <Const>reject</Const>
          <Const>John</Const>
          <Var>item</Var>
        </Uniterm>
      </then>
      <if>
        <And>
          <Uniterm>
            <Const>perishable</Const>
            <Var>item</Var>
          </Uniterm>
          <Uniterm>
            <Const>delivered</Const>
            <Var>item</Var>
            <Var>deliverydate</Var>
            <Const>John</Const>
          </Uniterm>
          <Uniterm>
            <Const>scheduled</Const>
            <Var>item</Var>
            <Var>scheduledate</Var>
          </Uniterm>
          <Uniterm>
            <Const>timediff</Const>
            <Var>diffdate</Var>
            <Var>deliverydate</Var>
            <Var>scheduledate</Var>
          </Uniterm>
          <Uniterm>
            <Const>greaterThan</Const>
            <Var>diffdate</Var>
            <Const>10</Const>
          </Uniterm>
        </And>
      </if>
    </Implies>
  </formula>
</Forall>

SEMANTICS

Interpretation and Models of Rules

Section Positive Conditions defined the notion of semantic structures and how such structures determine truth values of RIF conditions. The current section defines what it means for such a structure to satisfy a rule.

While semantic structures can be multivalued in RIF dialects that extend the core, rules are typically two-valued even in dialects that support inconsistency and uncertainty. Consider a rule of the form Q then :- if, where Q is a quantification prefix for all the variables in the rule. For the Horn subset, Q is a universal prefix, i.e., all variables in the rule are universally quantified outside of the rule. We first define the notion of rule satisfaction without the quantification prefix Q:

I |= then :- if

iff ITV(then) ≥t ITV(if). (Recall that the sef of truth values, TV, has a partial order ≥t.)

We define I |= Q then :- if iff I* |= then :- if for every I* that agrees with I everywhere except possibly on some variables mentioned in Q. In this case we also say that I is a model of the rule. I is a model of a rule set R if it is a model of every rule in the set, i.e., if it is a semantic structure such that I |= r for every rule r ∈ R.

The above defines the semantics of RIF Core using standard first-order semantics for Horn clauses. Various RIF dialects will extend this semantics in the required directions. Some of these extended semantics might not have a model theory (for example, production rules) and some will have non-first-order semantics. However, all these extensions are required to be compatible with the above definition when the rule set is completely covered by RIF Core.

=== Intended Models of Rules ===

The notion of a model is only the basic ingredient in the definition of a semantics of a rule set. In general, a semantics of a rule set R is the set of its intended models (see Y. Shoham. Nonmonotonic logics: meaning and utility. In: Proc. 10th International Joint Conference on Artificial Intelligence, Morgan Kaufmann, pp. 388--393, 1987). There are different theories of what the intended sets of models are supposed to look like depending on the features of the particular rule sets.

For Horn rules, which we use in this section, the intended set of models of R is commonly agreed upon: it is the set of all models of R.

However, when rule bodies contain literals negated with the negation-as-failure connective naf, then only some of the models of a rule set are viewed as intended. This issue will be addressed in the appropriate dialects of RIF. The two most common theories of intended models are based on the so called well-founded models and stable models. Here we will just illustrate the problem with a simple example.

Suppose R consists of a single rule p :- naf q. If naf were interpreted as classical negation, not, then this rule would be simply equivalent to p \/ q, and so it would have two kinds of models: one in which p is true and one where q is true. In contrast to first-order logic, most rule-based systems do not consider p and q symmetrically. Instead, they view the rule p :- naf q as a statement that p must be true if it is not possible to establish the truth of q. Since it is, indeed, impossible to establish the truth of q, such theories will derive p even though it does not logically follow from p \/ q. The logic underlying rule-based systems also assumes that only the minimal models as intended (minimality here is with respect to the set of true facts). Therefore, the intended models of the above rule set R must have the property that not only p is true but also that q is false.

4. RIF Compatibility

(Editor's Note: This text is maintained on wiki page RIF Compatibility).

The compatibility of RIF Core is currently focussed on the Semantic Web standards OWL and RDF, as explained in RIF-OWL Compatibility and RIF-RDF Compatibility.

4.1. RIF-OWL Compatibility

(Editor's Note: This text is maintained on wiki page RIF-OWL Compatibility).

RIF-OWL Compatibility will be described here on the basis of OWL Compatibility, A.5 Extension: Ontology Conditions, and (email) discussions.

4.2. RIF-RDF Compatibility

(Editor's Note: This text is maintained on wiki page RIF-RDF Compatibility).

RIF-RDF Compatibility will be described here on the basis of RDF Compatibility, A.4 Extension: Resource Conditions, and (email) discussions.

5. Appendix: RIF Validation

(Editor's Note: This text is maintained on wiki page Appendix: RIF Validation).

Validation of Positive Conditions

The BNF for Positive Conditions can be directly rewritten as a DTD (see PositiveConditions.dtd) or an XML Schema.

Using the DTD spec, XML validators such as Richard Goerwitz' STG Validator succeed with positive conditions such as the conjunction of Example 2b (see Positive Conditions):

<?xml version="1.0" standalone="no"?>
<!DOCTYPE And SYSTEM "http://www.jdrew.org/rif/PositiveConditions.dtd">
<And>
  ... valid content such as Example 2b ...
</And>

Validation of Horn Rules

The BNF for Horn Rules can be directly rewritten as a DTD (see HornRules.dtd) or an XML Schema.

Using the DTD spec, XML validators succeed with Horn clauses such as the clause of Example 4 (see Horn Rules):

<?xml version="1.0" standalone="no"?>
<!DOCTYPE Forall SYSTEM "http://www.jdrew.org/rif/HornRules.dtd">
<Forall>
  ... valid content such as Example 4 ...
</Forall>

END OF DOCUMENT. WIKI-TR diagnostics:

Warning: SGML2PL(sgml): []:12: Element "span" not allowed here
Warning: SGML2PL(sgml): []:14: Element "span" not allowed here
Warning: SGML2PL(sgml): []:16: Element "span" not allowed here
Warning: SGML2PL(sgml): []:18: Element "span" not allowed here
WARNING: missing otherStatus
retreiving 'Overview'...
Warning: SGML2PL(sgml): []:4: Element "span" not allowed here
Warning: SGML2PL(sgml): []:4: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:4: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:4: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:4: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:4: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:4: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:6: Element "span" not allowed here
Done.
retreiving 'Conditions'...
Warning: SGML2PL(sgml): []:4: Element "span" not allowed here
Done.
retreiving 'Positive_Conditions'...
Warning: SGML2PL(sgml): []:4: Element "span" not allowed here
Warning: SGML2PL(sgml): []:8: Element "span" not allowed here
ERROR: SGML2PL(sgml): []:8: Syntax error: Bad attribute list, found "/"
Warning: SGML2PL(sgml): []:12: Element "span" not allowed here
Warning: SGML2PL(sgml): []:24: Element "span" not allowed here
Warning: SGML2PL(sgml): []:26: Element "span" not allowed here
Warning: SGML2PL(sgml): []:28: Element "span" not allowed here
Warning: SGML2PL(sgml): []:30: Element "span" not allowed here
Warning: SGML2PL(sgml): []:32: Element "span" not allowed here
Warning: SGML2PL(sgml): []:82: Element "span" not allowed here
Warning: SGML2PL(sgml): []:82: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:82: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:82: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:82: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:82: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:82: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:82: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:82: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:82: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:82: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:82: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:82: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:82: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:82: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:82: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:82: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:84: Element "span" not allowed here
Warning: SGML2PL(sgml): []:84: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:84: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:84: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:84: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Element "span" not allowed here
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:86: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:86: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:88: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:88: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:88: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:88: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:90: Element "span" not allowed here
Warning: SGML2PL(sgml): []:92: Element "span" not allowed here
Warning: SGML2PL(sgml): []:96: Element "span" not allowed here
Warning: SGML2PL(sgml): []:96: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:96: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:98: Element "span" not allowed here
Warning: SGML2PL(sgml): []:105: Element "span" not allowed here
Warning: SGML2PL(sgml): []:107: Element "span" not allowed here
Warning: SGML2PL(sgml): []:111: Element "span" not allowed here
Warning: SGML2PL(sgml): []:113: Element "span" not allowed here
Warning: SGML2PL(sgml): []:115: Element "span" not allowed here
Warning: SGML2PL(sgml): []:117: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:117: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:117: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:117: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:117: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:117: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:117: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:117: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:117: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:117: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:117: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:117: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:117: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:117: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:117: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:117: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:117: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:117: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:117: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:117: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:117: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:117: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:117: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:117: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:117: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:117: Ignored end-tag for "strong" which is not open
Done.
retreiving 'Rules'...
Done.
retreiving 'Horn_Rules'...
ERROR: SGML2PL(sgml): []:4: Syntax error: Bad attribute list, found "/"
Warning: SGML2PL(sgml): []:6: Element "span" not allowed here
Warning: SGML2PL(sgml): []:99: Element "span" not allowed here
Warning: SGML2PL(sgml): []:99: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:99: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:99: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:99: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:99: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:99: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:99: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:99: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:99: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:99: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:101: Element "span" not allowed here
Warning: SGML2PL(sgml): []:101: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:101: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:103: Element "span" not allowed here
Warning: SGML2PL(sgml): []:105: Element "span" not allowed here
Warning: SGML2PL(sgml): []:105: Inserted omitted end-tag for "strong"
Warning: SGML2PL(sgml): []:105: Ignored end-tag for "strong" which is not open
Warning: SGML2PL(sgml): []:107: Element "span" not allowed here
Warning: SGML2PL(sgml): []:109: Element "span" not allowed here
Done.
retreiving 'Compatibility'...
Done.
retreiving 'RIF-OWL_Compatibility'...
Done.
retreiving 'RIF-RDF_Compatibility'...
Done.
retreiving 'Validation'...
Done.