Based on RIF's positive conditions, this section defines Horn rules with optional calls to external (constraint) solvers for RIF (Phase 1).
SYNTAX
To specify Horn clauses with optional external calls we just need to add the following productions to the human-readable syntax of A.1 Basis: Positive Conditions:
. . .
HEAD ::= LITFORM
BODY ::= CONDIT
CALL ::= EXTFORM
Implies ::= HEAD ':-' BODY [ '&' CALL ]
CLAUSE ::= 'Forall' Var* '(' Implies ')' | 'Forall' Var* '(' HEAD ')'
where CONDIT and LITFORM are defined in A.1 Basis: Positive Conditions, EXTFORM is a call to an external (constraint) solver, & (pronounced 'WITH') is a conjunctive connective, and :- (pronounced 'IF') is an implication connective.
Rules are generated by the Implies production. Facts are generated by the HEAD production, where such a factual HEAD is regarded as a shorthand for a rule with an empty, hence true, conjunctive BODY condition of the form
Implies ::= HEAD ':-' And '(' ')'
Finally, a CLAUSE generates a universally closed rule or fact.
Note that, since CONDIT permits disjunction and existential quantification, the rules defined by the Implies production look more general than Horn. However, it is well-known that such extended rules reduce to Horn via a simple syntactic transformation.
The document RIF Use Cases and Requirements describes the use case "Negotiating eBusiness Contracts Across Rule Platforms", containing this first rule proposed in a hypothetical negotiation by some agent John:
If an item is perishable and it is delivered more than 10 days after the scheduled delivery date then the item will be rejected.
This can be formalized in human-readable syntax without external calls equivalently as follows, assuming the universal closure when generated directly by the Implies production (Example 3a), showing the universal closure when generated through the CLAUSE production (Example 3b), and transforming BODY-only variables to existentials as introduced in the language of A.1 Basis: Positive Conditions (Example 3c):
Example 3a (A RIF rule in human-readable syntax using implicit quantification):
In this rule, the HEAD is a user-defined relation of two arguments, one a constant.
The BODY is a conjunction of five Atoms, the first three user-defined relations, the
fourth and fifth built-in relations.
reject(John ?item) :-
And ( perishable(?item)
delivered(?item ?deliverydate)
scheduled(?item ?scheduledate)
timediff(?diffdate ?deliverydate ?scheduledate)
greaterThan(?diffdate 10) )
Example 3b (A RIF rule in human-readable syntax using explicit top-level quantification):
In this rule, the HEAD is a user-defined relation of two arguments, one a constant.
The BODY is a conjunction of five Atoms, the first three user-defined relations, the
fourth and fifth built-in relations.
Forall ?item ?deliverydate ?scheduledate ?diffdate
(
reject(John ?item) :-
And ( perishable(?item)
delivered(?item ?deliverydate)
scheduled(?item ?scheduledate)
timediff(?diffdate ?deliverydate ?scheduledate)
greaterThan(?diffdate 10) )
)
Example 3c (A RIF rule in human-readable syntax using existential BODY quantification):
In this rule, the HEAD is a user-defined relation of two arguments, one a constant.
The BODY is a conjunction of five Atoms, the first three user-defined relations, the
fourth and fifth built-in relations.
Forall ?item
(
reject(John ?item) :-
Exists ?deliverydate ?scheduledate ?diffdate
(
And ( perishable(?item)
delivered(?item ?deliverydate)
scheduled(?item ?scheduledate)
timediff(?diffdate ?deliverydate ?scheduledate)
greaterThan(?diffdate 10) )
)
)
This can also be formalized in human-readable syntax with external calls as follows (only one is given from which the other two can be reconstructed):
Example 3b' (A RIF rule in human-readable syntax using explicit top-level quantification and with external call):
In this rule, the HEAD is a user-defined relation of two arguments, CLP-style distinct variables.
The BODY is a conjunction of three Atoms, all user-defined relations. The CALL is a conjunction of
an equational constraint (replacing the HEAD unification of Example 3b) and two 'built-out'
temporal-arithmetic constraints (replacing the BODY built-ins of Example 3b).
Forall ?agent ?item ?deliverydate ?scheduledate ?diffdate
(
reject(?agent ?item) :-
And ( perishable(?item)
delivered(?item ?deliverydate)
scheduled(?item ?scheduledate) )
&
And ( ?agent=John
timediff(?diffdate ?deliverydate ?scheduledate)
greaterThan(?diffdate 10) )
)
Notice that slotted forms can be combined with external calls, although slots are not used in the above examples. Actually, as sketched in F2F4 Breakout Slides, external calls (to special equational constraint solvers) can be used to unify slotted forms.
An XML syntax can be obtained from the above BNF and from A.1 Basis: Positive Conditions as follows:
. . . - head (consequent role, containing LITFORM) - body (antecedent role, containing CONDIT) - call (external role) - Implies (implication, containing head, body, and call roles in any order) - Forall (quantified CLAUSE formula with 'Forall')
This can be directly rewritten as a DTD (HornRules.dtd) or an XML Schema.
The rule in Example 3b can be serialized in XML, e.g. again having the head first, as shown below (since serializations are to be explicit, no direct serialization of Example 3a is offered, while the serialization of Example 3c is offered but not shown here).
Example 4 (A RIF rule in XML syntax):
<Forall>
<Var>item</Var>
<Var>deliverydate</Var>
<Var>scheduledate</Var>
<Var>diffdate</Var>
<Implies>
<head>
<Atom>
<Rel>reject</Rel>
<Con>John</Con>
<Var>item</Var>
</Atom>
</head>
<body>
<And>
<Atom>
<Rel>perishable</Rel>
<Var>item</Var>
</Atom>
<Atom>
<Rel>delivered</Rel>
<Var>item</Var>
<Var>deliverydate</Var>
</Atom>
<Atom>
<Rel>scheduled</Rel>
<Var>item</Var>
<Var>scheduledate</Var>
</Atom>
<Atom>
<Rel>timediff</Rel>
<Var>diffdate</Var>
<Var>deliverydate</Var>
<Var>scheduledate</Var>
</Atom>
<Atom>
<Rel>greaterThan</Rel>
<Var>diffdate</Var>
<Con>10</Con>
</Atom>
</And>
</body>
</Implies>
</Forall>
The rule in Example 3b' can be serialized in XML, e.g. adding the call last, as shown below, where we assume that the external solver accepts the serialization of RIF itself for the conjunction of equational and temporal-arithmetic constraints.
Example 4' (A RIF rule with external call in XML syntax):
<Forall>
<Var>agent</Var>
<Var>item</Var>
<Var>deliverydate</Var>
<Var>scheduledate</Var>
<Var>diffdate</Var>
<Implies>
<head>
<Atom>
<Rel>reject</Rel>
<Var>agent</Var>
<Var>item</Var>
</Atom>
</head>
<body>
<And>
<Atom>
<Rel>perishable</Rel>
<Var>item</Var>
</Atom>
<Atom>
<Rel>delivered</Rel>
<Var>item</Var>
<Var>deliverydate</Var>
</Atom>
<Atom>
<Rel>scheduled</Rel>
<Var>item</Var>
<Var>scheduledate</Var>
</Atom>
</And>
</body>
<call>
<And>
<Equal>
<Var>agent</Var>
<Con>John</Con>
</Equal>
<Atom>
<Rel>timediff</Rel>
<Var>diffdate</Var>
<Var>deliverydate</Var>
<Var>scheduledate</Var>
</Atom>
<Atom>
<Rel>greaterThan</Rel>
<Var>diffdate</Var>
<Con>10</Con>
</Atom>
</And>
</call>
</Implies>
</Forall>
Using the DTD spec, Richard Goerwitz' STG Validator succeeds with the Horn clause of Example 4:
<?xml version="1.0" standalone="no"?> <!DOCTYPE Forall SYSTEM "http://www.jdrew.org/rif/HornRules.dtd"> <Forall> ... content of Example 4 ... </Forall>
SEMANTICS
TO BE EXTENDED TO EXTERNAL CALLS.
Interpretation and Models of Rules
In A.1 Basis: Positive Conditions we defined the notion of semantic structures and what it means for such a structure to satisfy a RIF condition. Here we extend this notion and define what it means for such a structure to satisfy a rule.
While semantic structures can be multivalued, rules are typically two-valued even in logics that support inconsistency and uncertainty. Consider a rule of the form Q head :- body, 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 |= head :- body |
iff I(head) ≥ I(body).
We define I |= Q head :- body iff I* |= head :- body 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.
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 different rule sets.
For Horn rules, which we use in this section, the intended set of models of R is commonly agreed agreed upon: it is the set of all models of R.
However, when rules contain negation-as-failure (naf) literals in the body only some of the models of a rule set are accepted as intended. This issue will be addressed in future extensions 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 an example.
Suppose R has a single rule p :- naf q. If naf is interpreted as classical negation, not, then this rule is simply p \/ q, and so it has two kinds of models: one in which p is true and one where q is true. In contrast, most current rule-based systems do not consider p and q symmetrically. Instead, they view this as a specification of an intent 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 :- not q. The logic underlying rule-based systems also considers that only the minimal models as intended (minimality here means minimization of the set of true facts). Therefore, the intended models of our rule set must have the property that not only p is true but also that q is false.
Back: B. Extension: RIF Rule Language --- Root: CORE --- Next: CORE