This section defines Horn rules for RIF Phase 1. The syntax and semantics incorporates RIF Positive Conditions defined in Section Positive Conditions.
Syntax
Rules
A rule is a statement of the form conclusion :- condition, where conclusion is a non-builtin atomic well-formed formula (i.e., formula with signature atomic but not bi_atomic); condition is a well-formed condition formula as defined in Sections Symbols and Signatures and Slotted Terms and Frames. All free variables in a rule are explicitly universally quantified outside of the rule. RIF also allows explicit existential quantification in the condition of the rules (for variables that occure only in the condition), but this is known to be equivalent to universal quantification outside of the rule due to the tautology (Forall ?X conclusion :- condition) ≡ (conclusion :- Exists ?X condition), if ?X occurs in condition only.
EBNF for the Presentation Syntax
The overall structure of the syntax used in the RIF-BLD Horn rule sublanguage can be depicted using the following diagram, which extends the diagram shown in Section Positive Conditions.
The class Ruleset contains zero or more RULEs, where each RULE is one of the following classes:
Implies, which distinguishes if-CONDITION from then-ATOMIC parts (where ATOMIC represents the conclusion of the rule)
ATOMIC, which represents facts
Forall, which is specified through its parts, i.e. one or more variable (Var) declarations and, recursively, a RULE as the formula in their scope
Although not reflected in the diagram above or the EBNF syntax below, RIF requires explicit quantification of all variables. Therefore, variables that are not explicitly quantified in CONDITION must explicitly appear under a Forall.
The syntactic classes Var, CONDITION, and ATOMIC were specified in Section Positive Conditions.
The presentation syntax for Horn rules extends the syntax for Positive Conditions with the following productions.
EBNF grammar Ruleset ::= RULE* RULE ::= ' Forall ' Var+ ' ( ' RULE ' ) ' | 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 the premise CONDITION is true then the conclusion 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). The RULE production generates a rule or fact, possibly universally closed.
Note that, by definition, atomic formulas that correspond to builtin predicates (i.e., formulas with signature bi_atomic) are not allowed in the rule conclusions. This restriction is not reflected in the diagram or EBNF syntax above.
A ruleset is a set of RIF rules; it is generated by the production Ruleset.
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 iff its ATOMIC part is a well-formed atomic formula and the CONDITION part is a well-formed condition formula.
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 5 (A RIF rule in the presentation syntax) Here we use the prefix ppl as an abbreviation for http://example.com/people#. The prefix op is used for a yet-to-be-determined IRI, which will be used for RIF builtin predicates. a. Universal form: Forall ?item ?deliverydate ?scheduledate ?diffduration ?diffdays ( reject^^rif:local ( ppl:John^^rif:iri ?item ) :- And ( perishable^^rif:local ( ?item ) delivered^^rif:local ( ?item ?deliverydate ppl:John^^rif:iri ) scheduled^^rif:local ( ?item ?scheduledate ) fn:subtract-dateTimes-yielding-dayTimeDuration ( ?deliverydate ?scheduledate ?diffduration ) fn:get-days-from-dayTimeDuration ( ?diffduration ?diffdays ) op:numeric-greater-than ( ?diffdays 10 ) ) ) b. Universal-existential form: Forall ?item ( reject^^rif:local ( ppl#John^^rif:iri ?item ) :- Exists ?deliverydate ?scheduledate ?diffduration ?diffdays ( And ( perishable^^rif:local ( ?item ) delivered^^rif:local ( ?item ?deliverydate ppl:John^^rif:iri ) scheduled^^rif:local ( ?item ?scheduledate ) fn:subtract-dateTimes-yielding-dayTimeDuration ( ?deliverydate ?scheduledate ?diffduration ) fn:get-days-from-dayTimeDuration ( ?diffduration ?diffdays ) op:numeric-greater-than ( ?diffdays 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
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.
Classes, roles and their intended meaning - Ruleset (rule collection, containing rule roles) - 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 5a 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 6 (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>diffduration</Var></declare> <declare><Var>diffdays</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">ppl: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">fn:subtract-dateTimes-yielding-dayTimeDuration</Const></op> <arg><Var>deliverydate</Var></arg> <arg><Var>scheduledate</Var></arg> <arg><Var>diffduration</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:local">fn:get-days-from-dayTimeDuration</Const></op> <arg><Var>diffduration</Var></arg> <arg><Var>diffdays</Var></arg> </Uniterm> </formula> <formula> <Uniterm> <op><Const type="rif:iri">op:numeric-greater-than</Const></op> <arg><Var>diffdays</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">ppl: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">ppl:Fred</Const></arg> <arg><Var>item</Var></arg> </Uniterm> </then> </Implies> </formula> </Forall> </rule> </Ruleset>
Translation Between the Presentation and the XML Syntaxes
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 ( clause_{1} . . . clause_{n} ) | <Ruleset> <rule>clause_{1}</rule> . . . <rule>clause_{n}</rule> </Ruleset> |
Forall variable_{1} . . . variable_{n} ( rule ) | <Forall> <declare>variable_{1}</declare> . . . <declare>variable_{n}</declare> <formula>rule</formula> </Forall> |
conclusion :- condition | <Implies> <if>condition</if> <then>conclusion</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, iff it is a model of every rule in the set, i.e., iff it is a semantic structure such that I |= r for every rule r ∈ R.
The above defines the semantics of RIF BLD 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 BLD. This means that the set of intended models of such a rule set with respect to the extending dialect must coincide with the intended models defined by RIF BLD. For further details on defining the semantics for RIF dialects see end note on intended models for rule sets.
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 |= φ |
iff for every semantic structure I, such that I |= S, it is the case that I_{truth}(φ)=t.