|
View:
New views
3 Messages
—
Rating Filter:
Alert me
|
|
|
questions about the topObjectProperty
|
|||||||||||||||
|
|
Re: questions about the topObjectPropertyI hope that this post is not misplaced but I thought I would give some context about the Protege reference. Protege 4.0 is currently in transition and does not fully support OWL 2.0. Roughly speaking Protege 4.0 supports OWL 1.1. Protege 4.1, which will be released as an early alpha soon, does support OWL 2.0 and works with Hermit. -Timothy On Nov 4, 2009, at 7:30 PM, Wael Yehia wrote: > Hello everyone, > I'm trying to use some reasoner that supports OWL 2, fully, and > I'm particularly interested in being able to reason with the > Universal Role (represented by the topObjectProperty), the role that > relates every pair of individuals in the domain. > Now, I noticed that Protege 4.0 does not have a keyword for > topObjectProperty or at least it is not predefined and appear at the > root of the property hierarchy, the way the Thing (top) concept is > predefined and is at the root of the concept hierarchy. Maybe > because protege 4.0 doesn't support OWL 2 fully yet. And creating a > new property with the 'topObjectProperty' name won't make it the > topObjectProperty that we need but just some another property, > because by looking at the rdf output when you save the ontology > you'll see that the topObjectProperty that you defined is prefixed > with your ontology's name and not the 'owl:' prefix which is > presumably the right one. > I wrote some test cases manually, this is one of them in First Order > Logic (FOL): > (\forall x.F(x)) \and \not (\exist x.F(x)) > which is equal to: \forall x.False > I am not sure if this formula is satisfiable, maybe if the domain is > empty. But it can be translated to Description Logic (DL) using the > Universal Role (topObjectProperty) and becomes > \forall U. Bot > or in manchester syntax: > topObjectProperty only Nothing > > Now, my concern is that I'm not 100% sure that I'm expressing the > formula in RDF syntax (which i will show below) correctly, and > therefore don't know how Hermit 1.0 (which claims that it supports > OWL 2) is understanding it. So, if anyone knows whether this is > correct syntax, or knows anything about Hermit's reasoning > capabilities with topObjectProperty, then any advice or hints are > greatly appreciated. This is my RDF syntax ontology, I don't know if > I should include parts of it here or all of it, so I decide to put > it all here, and please note that I cheated a bit and used protege > to output it for me and then i manually changed the occurrences of > topobjectproperty with two version of my own: > 1) #TopObjectProperty .... I tried this one because protege shows > it as a super property of any new property you create so I thought > maybe it recognizes it this way > 2) owl:topObjectProperty > > This is the RDF ontology: > > > <?xml version="1.0"?> > <!DOCTYPE rdf:RDF [ > <!ENTITY owl2 "owl:" > > <!ENTITY owl "http://www.w3.org/2002/07/owl#" > > <!ENTITY xsd "http://www.w3.org/2001/XMLSchema#" > > <!ENTITY owl2xml "http://www.w3.org/2006/12/owl2-xml#" > > <!ENTITY rdfs "http://www.w3.org/2000/01/rdf-schema#" > > <!ENTITY rdf "http://www.w3..org/1999/02/22-rdf-syntax-ns#" > > <!ENTITY O3 "http://www.semanticweb.org/ontologies/2009/9/ > O3.owl#" > > ]> > <rdf:RDF xmlns="http://www.semanticweb.org/ontologies/2009/9/O3.owl#" > xml:base="http://www.semanticweb.org/ontologies/2009/9/O3.owl" > xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#" > xmlns:owl2xml="http://www.w3.org/2006/12/owl2-xml#" > xmlns:owl="http://www.w3.org/2002/07/owl#" > xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" > xmlns:owl2="owl:" > xmlns:O3="http://www.semanticweb.org/ontologies/2009/9/O3.owl#"> > <owl:Ontology rdf:about=""/> > > <!-- > /////////////////////////////////////////////////////////////////////////////////////// > // > // Object Properties > // > /////////////////////////////////////////////////////////////////////////////////////// > --> > > <!-- http://www.semanticweb.org/ontologies/2009/9/O3.owl#TopObjectProperty > --> > <owl:ObjectProperty rdf:about="#TopObjectProperty"/> > > <!-- owl:topObjectProperty --> > <owl:ObjectProperty rdf:about="owl:topObjectProperty"/> > > <!-- > /////////////////////////////////////////////////////////////////////////////////////// > // > // Classes > // > /////////////////////////////////////////////////////////////////////////////////////// > --> > > <!-- http://www.semanticweb.org/ontologies/2009/9/O3.owl#A --> > <owl:Class rdf:about="#A"/> > > <!-- http://www.semanticweb.org/ontologies/2009/9/O3.owl#Last --> > <owl:Class rdf:about="#Last"> > <owl:equivalentClass> > <owl:Class> > <owl:intersectionOf rdf:parseType="Collection"> > <owl:Class> > <owl:complementOf> > <owl:Restriction> > <owl:onProperty > rdf:resource="#TopObjectProperty"/> > <owl:someValuesFrom > rdf:resource="#b"/> > </owl:Restriction> > </owl:complementOf> > </owl:Class> > <owl:Restriction> > <owl:onProperty > rdf:resource="#TopObjectProperty"/> > <owl:allValuesFrom rdf:resource="#b"/> > </owl:Restriction> > </owl:intersectionOf> > </owl:Class> > </owl:equivalentClass> > </owl:Class> > > > > <!-- http://www.semanticweb.org/ontologies/2009/9/O3.owl#b --> > > <owl:Class rdf:about="#b"> > <owl:equivalentClass> > <owl:Class> > <owl:intersectionOf rdf:parseType="Collection"> > <rdf:Description rdf:about="#A"/> > <rdf:Description rdf:about="&owl;Thing"/> > </owl:intersectionOf> > </owl:Class> > </owl:equivalentClass> > </owl:Class> > > > > <!-- http://www.semanticweb.org/ontologies/2009/9/O3.owl#c --> > > <owl:Class rdf:about="#c"> > <owl:equivalentClass> > <owl:Class> > <owl:intersectionOf rdf:parseType="Collection"> > <owl:Class> > <owl:complementOf> > <owl:Restriction> > <owl:onProperty > rdf:resource="owl:topObjectProperty"/> > <owl:someValuesFrom > rdf:resource="#b"/> > </owl:Restriction> > </owl:complementOf> > </owl:Class> > <owl:Restriction> > <owl:onProperty > rdf:resource="owl:topObjectProperty"/> > <owl:allValuesFrom rdf:resource="#b"/> > </owl:Restriction> > </owl:intersectionOf> > </owl:Class> > </owl:equivalentClass> > </owl:Class> > > <!-- http://www.w3.org/2002/07/owl#Thing --> > > <owl:Class rdf:about="&owl;Thing"/> > </rdf:RDF> > <!-- Generated by the OWL API (version 2.2.1.1138) http://owlapi.sourceforge.net > --> > > > > > > finally, I was wondering if there is a formula containing a > topObjectProperty that is, say unsatisfiable, and if all occurences > of topObjectProperty are substituted by another property R, then it > becomes satisfiable. So, what I 'm asking is if there's an example > which clearly shows the distinction between a topObjectProperty and > an ordinary property, also I'm interested in logic (or maybe DL) > based satisfiability, and not satisfiability based on domain, range > or something else. > I was told that domain closure formulas such as \forall x.(F(x) <=> > (x=a | x=b)), can be used to distinguish between the > topObjectProperty and other properties, so this formula should be > unsatisfiable: > C(a) & C(b) & \forall x (C(x) <=> x=a) > which is equivalent to: > Ex.(C(x) & x=a) & Ex.(C(x) & x=b) & Ax.( (C(x) & x=a) | > (~C(x) & ~x=a) ) > So I translated them to a DL called ALCO+U, which allows nominals > and the Universal Role, using the translation: > Ex.C(x) becomes in DL \exist U. C > Ax.C(x) becomes in DL \forall U. C > where U is the universal role. And the other translations are > straightforward, such as x=a becomes {a}, and so on.. > Also, we assumed Unique Names Axioms in the above formula, but we > need to explicitly mention that in OWL 2, so I used the > DifferentIndividuals axiom to say that 'a' and 'b' are different > individuals. > This is that formula in Manchester Syntax: > topObjectProperty some (C and {a}) > and topObjectProperty some (C and {b}) > and topObjectProperty only ((not C) or {a}) > > So, after saying that 'a' and 'b' are distinct individuals, the > formula is found unsatisfiable, which is correct, but when replacing > topObjectProperty with another property, say R, the > unsatisfiablility stays, which after some thinking I found it > correct too. So this result made me write this email to ask for > advice about whether the topObjectProperty can be distinguished from > another role R using purely FOL semantics. > > Thank you. > > Wael > |
|||||||||||||||
|
|
Re: questions about the topObjectProperty2009/11/5 Wael Yehia <wmyehia2001@...>
Protege 4.0 is not really OWL 2 ready. You would need Protege 4.1, which is not yet officially released. We just released HermiT 1.1 and from the HermiT website, you can also get a compiled version of Protege 4.1 (no support and no guarantee that it is working, it is not an official Protege release).
Yes, without the owl prefix it is not really the top property.
That can directly be expressed as a DL axiom: SubClassOf(owl:Thing :F) SubClassOf(owl:Thing ObjectComplementOf(:F)) in other syntax top implies F top implies not F (I used two axioms because in your example the two x are not really the same, you could rename one into y due to the quantifier scope)
not equal, but it follows
The domain is required to be non-empty, so it is unsatisfiable.
No need for the top role, as said above. All axioms apply to all individuals, they can be seen as usiversally quantified. If you use the top object property, your domain can still have one element, but that element cannot have a successor. The ontology is still satisfiable though.
HermiT understands what you say, but you probably don't want to use the top object property.
HermiT supports indeed all of OWL 2 including owl:topObjectProperty.
only the second one is the top object property. The first one is just a normal property for HermiT.
In your ontology instances of the class C cannot have any successors (there you used the real top property) and instances of class Last cannot have any http://www.semanticweb.org/ontologies/2009/9/O3.owl#TopObjectProperty successor, but can have other successors.
This just implies a=b, unless you have unique name assumption.
Again, no need for the universal role: C(a) C(b) C equals {a} in functional style syntax ClassAssertion(C a) ClassAssertion(C b) EquivalentClasses(C ObjectOneOf(a))
Well, it can be axiomatised, so you can replace the top object property by a fresh property and add a couple of axioms (the fresh property is a super property of all other axioms, etc.) and you have the same effect. You should use the top object property sparsely, because it can be computationally expensive and in all your examples it was not needed and rather the result of a wrong translation, so I suggest you read more about OWL semantics and maybe its relation to FOL. Maybe the OWL primer is helpful: http://www.w3.org/TR/owl2-primer/ Best regards, Birte
-- Dr. Birte Glimm, Room 306 Computing Laboratory Parks Road Oxford OX1 3QD United Kingdom +44 (0)1865 283529 |
| Free embeddable forum powered by Nabble | Forum Help |