disjoint property axioms cause HermiT to consider BOT as unsatisfiable

w3c-lbd-cg / bot

Building Topology Ontology

https://w3id.org/bot

53 stars 15 forks source link

disjoint property axioms cause HermiT to consider BOT as unsatisfiable #117

Closed vcharpenay closed 2 years ago

vcharpenay commented 2 years ago

Since v3, BOT includes disjointness axioms among symmetric properties. When reasoning on an existing building (Espace Fauriel, in Saint-Étienne) with HermiT, these axioms seem to cause unsatisfiability.

When importing BOT as is (v3.0 and above), reasoner.isConsistent() returns false. After commenting all axioms of the form :p owl:propertyDisjointWith :q, reasoner.isConsistent() becomes true.

The building description includes bot:adjacentZone and bot:intersectsZone statements.

vcharpenay commented 2 years ago

related issue: #24.

mathib commented 2 years ago

we decided in the second last LBD meeting to remove the owl:propertyDisjointWith statements, to relax BOT, so they will be removed in the next release. Instead, we would like to define best practices for using BOT with non-mandatory SHACL constraints. There are plans to make a BOT data graph of an example building where we also have the full 3D geometry as the 'origin'. If you have example situations that you encountered while creating the dataset, and you were not 100% sure if your interpretation is correct, please add them to the list here: https://github.com/w3c-lbd-cg/bot/issues/76#issuecomment-865248738

mathib commented 2 years ago

closed together with issue #24 . Please check the version_0.4.0 branch for the next release