2

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

stan_plogic
  • 113
  • 8

2 Answers2

3

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 )
                        ]
    ] .
logi-kal
  • 7,107
  • 6
  • 31
  • 43
  • Please take a look at my comment below as that seems to do the trick without needing to declare individual restrictions. – stan_plogic May 05 '21 at 18:30
  • @stan_plogic For some reason I took for granted that you were searching for an extensional solution. If you can modify your intensional axioms, that solution is clearly better. – logi-kal May 05 '21 at 20:51
  • I am still admiring your solution. Glad to hear there is a name for it...:) If you could add both the solutions to your answer, I will delete my comment below and accept your answer again. I can edit it, but it seems to put that on a review list as I am still a newbie on this platform. – stan_plogic May 05 '21 at 21:47
  • @stan_plogic To me, it is ok like this ;-) Anyway I realized the reason why I din't suggest you the FunctionalProperty solution. Basically I thought you were searching for a general solution for any kind of "minCardinality"/"cardinality" and you wanted to understand the main difference between them. – logi-kal May 06 '21 at 07:26
  • Fair enough. I will accept your answer, if for nothing else making me read on intensional vs extensional definitions :). Thanks for taking the time. Much appreciated. – stan_plogic May 07 '21 at 01:58
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.

stan_plogic
  • 113
  • 8