Re: questions about the topObjectProperty

I 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
>

Received on Thursday, 5 November 2009 17:44:02 UTC