From: Ian Horrocks <horrocks@cs.man.ac.uk>

Date: Thu, 5 Sep 2002 15:36:21 +0100 (BST)

Message-ID: <15735.27621.520935.639162@excalibur.inf.tu-dresden.de>

To: "Jeremy Carroll" <jjc@hplb.hpl.hp.com>

Cc: <www-webont-wg@w3.org>

Date: Thu, 5 Sep 2002 15:36:21 +0100 (BST)

Message-ID: <15735.27621.520935.639162@excalibur.inf.tu-dresden.de>

To: "Jeremy Carroll" <jjc@hplb.hpl.hp.com>

Cc: <www-webont-wg@w3.org>

On September 4, Jeremy Carroll writes: > > > I have just been reading one of the threads that went on while I was on > holiday. > > i.e. > OWL semantics > http://lists.w3.org/Archives/Public/www-webont-wg/2002Aug/thread.html#44 > and also the subthread > OWL semantics ( with focus on an axiomatization) > > If I have understood Ian correctly > > Point 1b: > > > > It should NOT be possible to use OWL/RDF statements to constrain the > > meaning of OWL/RDF syntax. E.g., if myTransitive is a sub-class of > > transitiveProperty, then instances of myTransitive should NOT be > > treated by OWL as transitive properties. If we go down this road, then > > we need a (HOL) reasoner even to parse the syntax of an OWL ontology, > > to determine what is being said, and to check that it is valid OWL. > ... > > It may even be IMPOSSIBLE to be sure that we > > have derived the complete syntactic meaning of an OWL ontology > > (because the language is undecidable). > > The alternative being that sound and complete reasoners are too difficult to > build. > > However, the view that complete reasoning is possible in DL is based on a > restricted idea of what reasoning is (largely class subsumption reasoning, > and consistency checking) Given a sufficiently expressive language (i.e., one like OWL), this doesn't represent any restriction w.r.t. what you ask for below, i.e., being able to determine if ontology O1 models ontology O2. This is trivially reducible to ontology consistency. > So Ian brought up the case in > > http://lists.w3.org/Archives/Public/www-webont-wg/2002Aug/0033.html > > of > > >This is wrong. The MT simply imposes a restriction that, in all > >models, the interpretation of a TransitiveProperty must be closed > >under transitivity. This does not mean that any property that is > >closed under transitivity in all models is necessarily a > >TransitiveProperty (such a situation could result from other causes, > >e.g., the properties interpretation being empty in all models, or the > >size of the domain being less than 3 in all models). > > I find the entailments view of reasoning fairly compelling: > - an OWL document entails another if every interpretation of the first is > also an interpretation of the second. > > A complete reasoner should be able to prove any valid entailment. > > Thus, either it is the case that "any property that is closed under > transitivity in all models is necessarily a TransitiveProperty", or it is > the case that the concept owl:TransitiveProperty is in the domain of > discourse in an RDF style. The normal way these things are handled in description and modal logics is to have a set of "frame axioms" that constrain the set of admissible interpretations. These frame axioms are not treated as part of the KB/theory. E.g., in multi-modal K4, the frame axioms state that the only admissible interpretations in those in which the interpretations of all modalities are transitively closed. Similarly for a DL, the frame axioms might state that there is a subset of the set of all property names (the transitive properties) whose interpretations must be transitively closed. The KB/theory therefore doesn't contain any axioms relating to properties, and so the question of entailments does not arise w.r.t. properties. Having said that, the expressive power of OWL means that entailment w.r.t. ontologies containing property inclusion and transitivity axioms is still trivially reducible to ontology consistency. Thus if we have a sound and complete reasoner for ontology consistency, we have a sound and complete reasoner for ontology entailment. The point w.r.t. transitive properties is simply that, if we don't take the frame axiom view, and decide instead that we can infer the transitivity of a role, then we need to be a little more careful about how we state the restriction w.r.t. the use of transitive properties in cardinality restrictions. This is not a serious problem - just something we have to take care of. It is a completely different thing if we can infer the existence of an axiom asserting that a property is transitive (as would be the case if OWL syntax were in the domain of discourse). In this case, we need to perform inference (in a language which is almost certainly undecidable) on the ontology in order to determine if it conforms with our definition of what is a syntactically valid ontology. I was suggesting (in point 1b) that we don't want to go there! Regards, Ian > So, I am increasingly coming round to thinking that incompleteness is > inevitable ... > > Jeremy > > > > >Received on Thursday, 5 September 2002 10:43:45 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:56:47 UTC
*