Re: OWL reasoning in rules

Dear all, let me first point out that, both in tableau-based and in  
resolution-based approaches to reasoning over OWL, "rules" are used:  
so-called "expansion rules" for the former. Also, you might find the  
following summary of  Section 3 from the paper I mentioned in my  
previous email helpful:

  ----
It is not too difficult to see that we can construct an OWL ontology  
all of whose models are infinite (let me know if you want  to see an  
example of such an ontology), e.g., where each model contains an  
infinite chain of fathers *in addition to the fathers that are  
explicitly present in the ontology, and hence we have to be careful  
if we want to ensure termination of a reasoning algorithm (without  
compromising its correctness) that checks for consistency/ 
satisfiability or answers queries. For OWL and many DLs, termination  
can be ensured without losing completeness because we can restrict  
our attention to certain “nice” models, e.g. to  tree models or to  
forest models.

Let us contrast these observations with the kind of reasoning  
required for function-free Horn rules. In such rules, all variables  
are universally quantified,
i.e. there are no existentially quantified variables in rule  
consequents.
Hence, we never have to infer the existence of “new” objects (such as  
infinite chains of fathers!). Thus, reasoning
algorithms must consider only individuals which are explicitly  
introduced and are given a name in the ontology. Reasoning can be  
performed
by grounding the rules, i.e. replacing the variables in the rules  
with all individuals
from the knowledge base in all possible ways. Through grounding,  
first-order reasoning becomes propositional since a ground rule is  
essentially
equivalent to a propositional clause. For a finite program, the  
number of
ground rules is also finite, and satisfiability of a set of  
propositional clauses is
decidable. Hence, the rules, such as the one defining hasAunt(x, y)  
from the
introduction, are allowed to enforce arbitrary but finite, non-tree  
models,
and not only “nice” models.

Now let us see what happens if we extend a description logic such as
SHIQ with function-free Horn rules. Then, we combine a logic whose  
decidability
is due to the fact that we can restrict our attention to “nice”
models (but with individuals whose existence may be implied by a  
knowledge
base) with the one whose decidability is due to the fact that we can
restrict our attention to “known” individuals (but with arbitrary  
relations
between them). Unsurprisingly, this and similar combinations are  
undecidable.
----

On 25 May 2007, at 11:48, Matt Williams wrote:

> Dear Ian, Ulrike & Bijan,
>
> Thank you so much for your speedy & comprehensive replies. To  
> clarify, I was indeed talking about using a rules engine to do OWL  
> reasoning; Bijan, you're right about the imprecision of what a  
> "rule" is (and I'm not clear, either. The work I'm doing at the  
> moment uses very simple horn-clause rules with variables that are  
> unified with terms from the ABox). Also, the distinction between  
> data-heavy and axiom heavy reasoning.
>
> The reason it came up was a) because it seems to be a perennial  
> problem and b) there seem to be some existing techniques (like  
> backward chaining) that I can't immediately see how one would  
> implement when your data is the ABox of an ontology.
>
> Thanks a lot,
>
> Matt
>

Ulrike Sattler
sattler@cs.man.ac.uk
http://www.cs.man.ac.uk/~sattler/

Received on Friday, 25 May 2007 11:17:52 UTC