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 `RULE`s, which are `Forall`-closed RIF `CLAUSE`s. 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**:

then :- if |

iff **I**_{Truth}(*then*) ≥_{t} **I**_{Truth}(*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

*that agrees with*

**I****everywhere except possibly on some variables mentioned in*

**I****Q**. In this case we also say that

*I*is a

*.*

**model of the rule***is a*

**I**

**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

*|= r for every rule r ∈*

**I****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.