Mixing EquivalentClass and SubClass in OWL

I'm curious about mixing SubClassOf and EquivalentClass in a Class description, and how a reasoner would behave.

Specifically, if I have both an EquivalentClass and a SubClassOf assertion for the same Class, do both the EquivalentClass AND the SubClassOf conditions need to be satisfied for an individual to be classified in that Class, or only the EquivalentClass?

Or is this a bad practice?

For example (Declarations omitted):

ObjectPropertyRange(:format :Bar)
ObjectPropertyRange(:format owl:Thing)
EquivalentClas开发者_StackOverflow中文版s(:Foo ObjectSomeValuesFrom(:format :Bar))
SubClassOf(:Foo :Sna)

I want to ensure that in the case below, :x is classified as :Foo, because both the EquivalentClass and SubClassOf assertions are satisfied:

ClassAssertion(:x :Sna)
ObjectPropertyAssertion(:format :x :someBar)

But :y is not, because the SubClassOf is not satisfied:

ClassAssertion(:y :NotASna)
ObjectPropertyAssertion(:format :y :someOtherBar)

Thanks,

Jonathan

I don't completely understand your question but I'll try to clarify some things. First of all, the following axioms seem irrelevant for your question (and the second is redundant anyway because owl:Thing is any property's range):

ObjectPropertyRange(:format :Bar)
ObjectPropertyRange(:format owl:Thing)

The other thing is that the EquivalentClasses-axioms can be seen as a syntactic sugar for SubClassOf-axioms, e.g.

EquivalentClasses(C1 C2)

is logically equivalent to

SubClassOf(C1 C2)
SubClassOf(C2 C1)

So you can rewrite your EquivalentClasses as:

SubClassOf(ObjectSomeValuesFrom(:format :Bar) :Foo)
SubClassOf(:Foo ObjectSomeValuesFrom(:format :Bar))

This would maybe simplify understanding of what entailments your ontology makes.

Now, if you say:

ClassAssertion(:x :Sna)
ObjectPropertyAssertion(:format :x :someBar)

I am assuming that you want to say:

ClassAssertion(:x :Sna)
ClassAssertion(:someBar :Bar)
ObjectPropertyAssertion(:format :x :someBar)

This entails that :x is both :Foo and :Sna, which is certainly possible because :Foo is a subclass of :Sna.

When you say

ClassAssertion(:y :NotASna)
ObjectPropertyAssertion(:format :y :someOtherBar)

I assume that you mean:

ClassAssertion(:y :NotASna)
ClassAssertion(:someOtherBar :Bar)
DisjointClasses(:NotASna :Sna)
ObjectPropertyAssertion(:format :y :someOtherBar)

This is a logical inconsistency because :y is entailed to be a :Foo (which is a subclass of :Sna), but at the same time :y is asserted to be in a class that is disjoint from :Sna.

Note also that we didn't use the knowledge that

SubClassOf(:Foo ObjectSomeValuesFrom(:format :Bar))

which followed from the EquivalentClasses-axiom.