Reasoning over OWL cardinality restriction

Question

I think I still have a fundamental misunderstanding of OWL axioms :(.

Here is a small test ontology I created:

@prefix xsd:      <http://www.w3.org/2001/XMLSchema#> .
@prefix rdf:      <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs:     <http://www.w3.org/2000/01/rdf-schema#> .
@prefix owl:      <http://www.w3.org/2002/07/owl#> .
@prefix :         <http://foobar.com/test/> .

: a owl:Ontology .

:prop1 a owl:DatatypeProperty .
:prop2 a owl:DatatypeProperty .

:Class1 owl:equivalentClass [
    a owl:Restriction ;
    owl:onProperty :prop1 ;
    owl:cardinality "1"^^xsd:int
  ] .

:Ind1 a owl:NamedIndividual ;
  :prop1 "value1"^^xsd:string .

:Class2 owl:equivalentClass [
    a owl:Restriction ;
    owl:onProperty :prop2 ;
    owl:minCardinality "1"^^xsd:int
  ] .

:Ind2 a owl:NamedIndividual ;
  :prop2 "value2"^^xsd:string .

When I run the Hermit reasoner in Protege over this, I get the expected result with :Ind2, that is it is a member of :Class2. But I am not getting the same for :Ind1 with regards to being a member of :Class1.

I am suspecting that this has to do with open world assumption and that it is possible that :Ind1 might still have another :prop1 assertion. So couple of questions:

• Have I diagnosed the problem correctly?
• Can I get an example of how I can get my goal for hermit to reason that :Ind1 is a member of :Class1 without explicitly making the assertion?

Thanks

Answer 1

Premise

OWL semantics is defined under open-world assumption, so you can't check if the cardinality for a certain property is exactly N, because there may be other property instances even if not declared.

More precisely, these are the checks that you can do:

Cardinality check	Possible answers	Sound	Complete
At-least N	Yes (if N or more) I don't know (otherwise)	Yes	No
Exactly N	No (if N+1 or more) I don't know (otherwise)	Yes	No
At-most N	No (if N+1 or more) I don't know (otherwise)	Yes	No

Solution

You can check if a cardinality is exactly 1 only if you explicitly state that "value1" is the only value for :Ind1. In this case :Ind1 will be part of :Class1.

In FOL:

∀x.(R(Ind1, x) → x = "value1")

In DL:

∃R⁻.{Ind1} ⊑ {"value1"}

In OWL2 (not tested):

:Ind1
  a owl:NamedIndividual ;
  a [ a                 owl:Restriction ;
      owl:onProperty    :prop1 ;
      owl:allValuesFrom [ a          rdfs:Datatype ;
                          owl:oneOf  ( "value1"^^xsd:string )
                        ]
    ] .

Answer 2

Thanks to @horcrux for providing the hint. What worked finally is to also declare the properties as owl:FunctionalProperty. Editing the property declarations to:

:prop1 a owl:DatatypeProperty, owl:FunctionalProperty .
:prop2 a owl:DatatypeProperty, owl:FunctionalProperty .

This does not require adding additional restrictions to each individual declaration.