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=""/>

    

    
    <owl:ObjectProperty rdf:about="#TopObjectProperty"/>

    
    <owl:ObjectProperty rdf:about="owl:topObjectProperty"/>

    

    
    <owl:Class rdf:about="#A"/>

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


    

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


    

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

    

    <owl:Class rdf:about="&owl;Thing"/>
</rdf:RDF>


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