- From: Ulrike Sattler <sattler@cs.man.ac.uk>
- Date: Fri, 25 May 2007 12:12:43 +0100
- To: Matt Williams <matthew.williams@cancer.org.uk>
- Cc: Ian Horrocks <horrocks@cs.man.ac.uk>, Owl Dev <public-owl-dev@w3.org>, Semantic Web <semantic-web@w3.org>, Bijan Parsia <bparsia@cs.man.ac.uk>
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