This section defines Horn rules for RIF Phase 1. The syntax and semantics incorporates RIF Positive Conditions defined in Section Positive Conditions.
Syntax
Abstract Syntax
The abstract syntax of the Horn rule language extending Positive Conditions is given in asn06 as follows:
class Ruleset
property formula : list of RULE
class RULE
subclass Forall
property declare : list of Var
property formula : CLAUSE
class CLAUSE
subclass ATOMIC
subclass Implies
property if: CONDITION
property then: ATOMIC
The abstract syntax is visualized by a UML diagram extending the UML diagram of Positive Conditions as shown below.
The central RIF Ruleset class contains zero or more RULEs, which are Forall-closed RIF CLAUSEs. The class Forall is specified through its parts, i.e. zero or more variable (Var) declarations and a CLAUSE formula, which can be an Implies or an ATOMIC formula. The Implies class distinguishes if-CONDITION from then-ATOMIC parts.
Upload new attachment "HornModel.png"
The classes Var, CONDITION, and ATOMIC were specified in the abstract syntax of Positive Conditions.
The combined RIF Core abstract syntax and its visualization are given in Appendix: Specification.
Concrete Syntax
The abstract syntax of Section Abstract Syntax can again be instantiated to a concrete syntax.
The concrete human-readable syntax, described in this EBNF extending the one for Positive Conditions by the following productions, is work in progress and under discussion:
Ruleset ::= RULE* RULE ::= 'Forall' Var* CLAUSE CLAUSE ::= Implies | ATOMIC Implies ::= ATOMIC ':-' CONDITION
Var, ATOMIC, 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 ATOMIC :- CONDITION should be informally read as if CONDITION is true then ATOMIC 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 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). 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.
Well-formed rules. A rule is well-formed if its ATOMIC part is a well-formed atomic formula and the CONDITION part is a well-formed condition formula.
The following examples of EBNF and XML rule syntax use the unsorted version of the condition syntax and do not illustrate the use of IRIs for predicates and concepts. This will be addressed in a future working draft.
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 EBNF 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 XML syntax of Positive Conditions, by serializing the above abstract syntax (and 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 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.
- Ruleset (collection of rules) - Forall (quantified formula for 'Forall', containing declare and formula roles) - Implies (implication, containing then and if roles in any order) - then (consequent role, containing ATOMIC) - if (antecedent role, containing CONDITION)
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>
<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>
<Forall>
<declare><Var>item</Var></declare>
<formula>
<Implies>
<then>
<Uniterm>
<Const>reject</Const>
<Const>Fred</Const>
<Var>item</Var>
</Uniterm>
</then>
<if>
<Uniterm>
<Const>unsolicited</Const>
<Var>item</Var>
</Uniterm>
</if>
</Implies>
</formula>
</Forall>
</Ruleset>
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 ITruth(then) ≥t ITruth(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. For further details on defining the semantics for RIF dialects see end note on intended models for rule sets.