This section defines rules for RIF BLD. The syntax and semantics incorporates RIF Positive Conditions defined in Section Positive Conditions.
Syntax
Formal Preliminaries
A rule is a statement of the form head :- body, where head is an atomic well-formed formula and body is a well-formed condition formula as defined in Sections Symbols and Symbol Spaces (Positive Conditions) and Symbols and Symbol Spaces (Slotted Conditions). All bound variables that occur in the rule are explicitly universally quantified.
Presentation Syntax
The overall structure of the syntax used in the RIF BLD Horn rule sublanguage is visualized by means of the following diagram, which extends the diagram shown in Section Positive Conditions.
The class Ruleset contains zero or more RULEs, which are universally quantified RIF clauses. This is represented by a RULE being either
an Implies, which distinguishes if-CONDITION from then-ATOMIC parts;
an ATOMIC formula, for representing facts, that is, Implies where the if-part is always true and is omitted, by convention;
or a Forall, recursively. The class Forall is specified through its parts, i.e. one or more variable (Var) declarations and a RULE as the formula in its scope. RIF does not allow implicitely quantified variables: all the variables that are implicitely universally quantified in an Implies or an ATOMIC MUST be within the scope of a Forall that declares them.
RIF Core thus enables the interchange of rules that are universally closed Horn clauses with one and only one positive literal, and where the universal quantifiers that are often left implicit are made explicit.
The syntactic classes Var, CONDITION, and ATOMIC were specified in the syntax of Positive Conditions. The complete RIF BLD conceptual structure can be visualised on the diagram given in Appendix Specification.
The presentation syntax for Horn rules extends the syntax for Positive Conditions with the following productions.
Ruleset ::= RULE* RULE ::= Forall | Implies | ATOMIC Forall ::=' Forall ' Var* ' ( ' RULE ' ) ' Implies ::= ATOMIC ' :- ' CONDITION
Var, ATOMIC, and CONDITION were defined as part of the syntax for positive conditions in Positive Conditions. Following the Logic Programming usage, the symbol :- denotes the implication connective used in rules. The statement ATOMIC :- CONDITION should be informally read as: "ATOMIC if CONDITION", that is, if CONDITION is true then ATOMIC is also true.
Rules are generated by the Implies production. Facts are generated by the ATOMIC production, and can be viewed as the then part of an Implies with an empty conjunctive if (or with true as the if part). The Forall production generates a universally closed rule or fact.
A ruleset is a set of RIF rules; it is generated by the production Ruleset.
*** Comment CSMA: aren't the above three paragraphs redundant and shouldn't they be removed (from "Var, ATOMIC, and CONDITION were defined as part..." to "... is generated by the production Ruleset.")? The paragraph below ("Note also that...") could then be inserted after the sentence: "The syntactic classes Var, CONDITION, and ATOMIC were specified in the syntax of Positive Conditions", above (befor ethe BNF for the presentation syntax). ***
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.
Well-formed rules. A rule is well-formed if its ATOMIC part is a well-formed atomic formula, its CONDITION part is a well-formed condition formula and all the variables are within the scope of a quantifier where they are declared.
The document RIF Use Cases and Requirements includes a use case "Negotiating eBusiness Contracts Across Rule Platforms", which discusses a business rule slightly modified here:
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 Presentation EBNF Syntax used throughout this document, this rule can be written in one of these two equivalent ways:
Example 3 (A RIF rule in the presentation syntax) a. Universal form: Forall ?item ?deliverydate ?scheduledate ?diffdate ( reject^^rif:local ( http://example.com/people#John^^rif:iri ?item ) :- And ( perishable^^rif:local ( ?item ) delivered^^rif:local ( ?item ?deliverydate http://example.com/people#John^^rif:iri ) scheduled^^rif:local ( ?item ?scheduledate ) timediff ( ?diffdate ?deliverydate ?scheduledate ) greaterThan ( ?diffdate 10 ) ) ) b. Universal-existential form: Forall ?item ( reject^^rif:local ( http://example.com/people#John^^rif:iri ?item ) :- Exists ?deliverydate ?scheduledate ?diffdate ( And ( perishable^^rif:local ( ?item ) delivered^^rif:local ( ?item ?deliverydate http://example.com/people#John^^rif:iri ) scheduled^^rif:local ( ?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. These two forms are logically equivalent.
XML Syntax
EDITORS' NOTE: The XML syntax for BLD presented here is one of the proposals the Working Group is considering. It is presented here to get feedback on this strawman and to give readers an idea for the kind of information that will be presented in this section.
The following extends the XML syntax of Positive Conditions, by serializing the above EBNF Syntax of RIF Horn rules 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 if and then to designate these two parts of a rule.
- Ruleset (collection of rules) - Forall (quantified formula for ' Forall ', containing declare and formula roles) - Implies (implication, containing if and then roles) - if (antecedent role, containing CONDITION) - then (consequent role, containing ATOMIC)
For the XML Schema Definition (XSD) of the RIF BLD Horn rule language see Appendix Specification.
For instance, the rule in Example 3a can be serialized in XML as shown below as the first element of a rule set whose second element is a business rule for Fred.
Example 4 (A RIF rule set in XML syntax) <Ruleset> <rule> <Forall> <declare><Var>item</Var></declare> <declare><Var>deliverydate</Var></declare> <declare><Var>scheduledate</Var></declare> <declare><Var>diffdate</Var></declare> <formula> <Implies> <if> <And> <formula> <Uniterm> <op><Const type="rif:local">perishable</Const></op> <arg><Var>item</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">delivered</Const></op> <arg><Var>item</Var></arg> <arg><Var>deliverydate</Var></arg> <arg><Const type="rif:iri">http://example.com/people#John</Const></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">scheduled</Const></op> <arg><Var>item</Var></arg> <arg><Var>scheduledate</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">timediff</Const></op> <arg><Var>diffdate</Var></arg> <arg><Var>deliverydate</Var></arg> <arg><Var>scheduledate</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:iri">http://www.w3.org/2007/rif/builtin/greaterThan</Const></op> <arg><Var>diffdate</Var></arg> <arg><Const type="xsd:long">10</Const></arg> </Uniterm> </formula> </And> </if> <then> <Uniterm> <op><Const type="xsd:long">reject</Const></op> <arg><Const type="rif:iri">http://example.com/people#John</Const></arg> <arg><Var>item</Var></arg> </Uniterm> </then> </Implies> </formula> </Forall> </rule> <rule> <Forall> <declare><Var>item</Var></declare> <formula> <Implies> <if> <Uniterm> <op><Const type="rif:local">unsolicited</Const></op> <arg><Var>item</Var></arg> </Uniterm> </if> <then> <Uniterm> <op><Const type="rif:local">reject</Const></op> <arg><Const type="rif:iri">http://example.com/people#Fred</Const></arg> <arg><Var>item</Var></arg> </Uniterm> </then> </Implies> </formula> </Forall> </rule> </Ruleset>
Syntax Translation
The translation between the presentation syntax and the XML syntax is given by a table that extends the translation tables of Positive Conditions and Slotted Conditions as follows.
Presentation Syntax | XML Syntax |
---|---|
Ruleset ( ?rule_{1} . . . ?rule_{n} ) | <Ruleset> <rule> ?rule_{1} </rule> . . . <rule> ?rule_{n} </rule> </Ruleset> |
Forall ?variable_{1} . . . ?variable_{n} ( ?body ) | <Forall> <declare> ?variable_{1} </declare> . . . <declare> ?variable_{n} </declare> <formula> ?body </formula> </Forall> |
?head :- ?body | <Implies> <if> ?body </if> <then> ?head </then> </Implies> |
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 BLD, 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 I_{Truth}(then) ≥_{t} I_{Truth}(if). (Recall that the set 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, denoted I |= 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.
Entailment of RIF Conditions by Rulesets
We will now define what it means for a set of rules to entail a RIF condition. Let S be a RIF ruleset and φ a closed RIF condition (a condition with no occurrences of free variables). Then we say that S entails φ, written as
S |= φ |
if for every semantic structure I, such that I |= S, it is the case that I_{truth}(φ)=t.