[UCR] RIF needs different reasoning methods

Dear All,

At the RIF meeting last week in Mandelieu, I have been asked to
explain the view that RIF needs different reasoning methods -
even though it should have a single declarative semantics.

The following is a (sketch of an) application scenario illustrating
different forms of reasoning with rulesets that, in my opinion, the
RIF should support.

Two software companies, Rule Experts and Semantics Corp, get
involved in a long term joint project. So as to have common
regulations concerning travel, Rule Experts and Semantics Corp
exchange their travel regulations expressed as RIF rules.

1. Rules for Aligning Vocabularies - A Case for Constructive
Reasoning with Deduction Rules

The vocabularies used in the travel regulation rules of Rule
Experts and of Semantics Corp are not identical. In a first phase,
both companies jointly align these vocabularies, i.e. specify
correspondences between concepts such as:

* a junior employee of Rule Experts acting as an area manager
corresponds a project leader at Semantics Corp.

A rule like the previous one is similar to a database view (also
called deduction rule): it gives rise to (deterministically) derive
new information from information explicitely stated. Simple and
efficient reasoning techniques (referred to as 'constructive
reasoning') are sufficient for this, especially no excluded middle or
refutation are needed. Such simple reasoning techniques are
e.g. forward chaining and backward chaining SLD resolution also called
(linear resolution without ancestor resolution) as used with
Datalog. Let refer to such rules as 'deduction rules'.

Dedicated RIF reasoners for deduction rules would be useful for
generating conclusions - either by forwards or backward chaining -
from deduction rules.

2. Computing Consequences, Consistency and Redundancy
Cheking - A Case for Full-Fledge Reasoning

After the vocabularies used in regulations from Rule Experts and
Semantics Corp have been aligned (using deduction rules), consequences
of the merged regulation are investigated like e.g. whether the
resulting merged travel regulation implies that junior employees are
not allow to fly first-class. To this aim a full-fledge reasoner,
i.e. a reasoner more powerful than the constructive reasoners
mentioned in the previous section, are needed. Such reasoners in
general must be capable of excluded middle and/or refutation and/or
similar proof techniques.

Furthermore, the merged travel regulation is investigated. More
precisely, a ruleset including the constructive rules aligning the
vocabularies and the regulations of each company (expressed as
rulesets) is checked for the following properties:

- logical consistency, i.e. the existence of models satisfying the
merged ruleset.

- a property one could call 'practical consistency', i.e. the
existence of 'meaningful' models satisfying the ruleset, e.g. models
in which no employee categories are empty.

- redundancy, i.e. whether some rules in the ruleset logically follow
from others.

The reasoning involved in checking the properties above is more
complex than that needed with constructive rules. It requires in
general excluded middle and/or refutation and/or similar proof
techniques.

Consistency and redundancy checking is performed by using another kind
of dedicated RIF reasoners. Note that these reasoners should
interprete negation monotonically, i.e. like classical logic negation,
as there are no references to a state of affairs (or database or
A-boxes) to which the closed world assumption could be applied.

3. Generation of Reactive Rules from Declarative Normative Rules - A
Case for Rule Transformation

Once a (logically and 'practically' cf. 2 above) consistent and
non-redundant ruleset has been found, its rules are used as follows
when project members from each company apply for business trips so as
to ensure that travel application that violate the merged travel
regulation of Rule Experts and Semantic Corp are rejected.

A simple evaluation of each rule each time a travel is applied for
would be very inefficient. An efficient evaluation of the travel
regulation is achieved by generating from each declarative rule of the
travel regulation ruleset a reactive rule ensuring an event-driven
evaluation of the declarative rule. An example illustrates this
generation. Assume a declarative rule (from the travel regulation
ruleset) stating the following:

* Travels of more than 200 km and of less than 5 days should be made
by train or plane.

Reactive rules like the following are generated that ensure an
efficient, event-driven enforcement of the above declarative rule:

* If a car travel is applied for, then it is granted only if it is
of more than 200 km and of less than 5

* If an extension of the duration of a formerly granted travel of
more than 5 days is applied for and if the granted travel was by
car, then the travel should no longer be granted.

A third kind of RIF tools, let call it a 'rule transformer', is needed
that generate from declarative rules expressed in the declarative
fragment of RIF reactive rules expressed in the reactive fragment of
RIF like.

Note that the evaluation of the antecedents of the reactive rule
generated should interprete negation non-monotonically, i.e. unlike
classical logic negation. Indeed, the evaluation of these reactive
rule antecedents refers to a state of affairs (or database or A-boxes)
based on a closed word assumption. This state of affairs consists in
the (already granted or not yet granted) travel applications.

4. Concluding Remarks

Event hough the declarative semantics of the constructive and of the
other declarative RIF rules of the application scenario sketched above
can be formalized in the same manner, e.g. by a Tarsky-style model
theory, different type of RIF reasoners and/or rule transformers are
needed.

Note that existing OWL reasoners only address 2 above. They can
perform 1 but at unnecessary costs. They cannot perform 3. The
techniques described under 1 and 3 are needed for many business rule
applications and have a considerable application potential on the Web.

Regards,

Francois

Received on Monday, 6 March 2006 08:50:28 UTC