Reflexive object properties in BFO2020

[Stefan Schulz]

I am wondering why in the current OWL version of BFO 2020 

'occurrent part of' is not marked as "reflexive"

According to the definition :

b 'proper occurrent part of' c =Def. 

    b 'occurrent part of' c & b and c are not identical [005-BFO]

the key difference between 

'occurrent part of' and  'proper occurrent part of' 

is exactly the reflexivity feature.  

I also do not understand why in the OWL version the former is marked as transitive and the latter isn't.  

Barry, Alan, could you explain?

Thanks!

Stefan

--

Stefan Schulz
Univ.-Prof. Dr. med.

Institute for Medical lnformatics, Statistics and Documentation
Medical University of Graz, Auenbruggerplatz 2/5
A-8036 Graz, Austria
Tel: +43 316 385 16939   |   +43 699 150 96 270  

Email:  stefan...@medunigraz.at
Web:   www.medunigraz.at/imi/  |  purl.org/steschu

[Chris Mungall]

Hi Stefan,

Reflexivity doesn’t play well with domain and range constraints. See the RO design pattern docs 

https://oborel.github.io/obo-relations/reflexivity/

BFO could however adopt the weaker local reflexivity constraint defined in RO. This is harder in OWL but trivial in FOL

--
You received this message because you are subscribed to the Google Groups "BFO Discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to bfo-discuss...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/bfo-discuss/CAHM_EAuXJvtGk43K9D1cMnb70h-HGZ2Purgx1q%3D-McU2w%3Dii4Q%40mail.gmail.com.

[Michael DeBellis]

I've used the Reflexive option for OWL properties on a couple of ontologies and I always ended up removing it. At least with the reasoners in Protege it makes reasoning very slow because regardless of how you define the domain and range they always end up being owl:Thing which means that if you define hasFoo to be reflexive the reasoner ends up asserting that for every individual x in your ontology x hasFoo x is true. It slows down the reasoner significantly in my experience and it just isn't practical for most ontologies. 

Michael

To view this discussion on the web visit https://groups.google.com/d/msgid/bfo-discuss/CAN9AifscVndTSEDwhvoNTCB0Qknbe%3Dgi%3DuN04bDbf58U%3DrA4eA%40mail.gmail.com.

[Chris Mungall]

Hi Michael,

I don't think making the reasoner too slow is ever a reason to remove an axiom from a reference ontology. I assume you are talking about complete DL reasoners like HermiT here. These are almost never used on the ontologies I work on because they are too slow, regardless of reflexivity axioms. There are a variety of strategies to use here, including selective removal of some axioms, but the removal should never be done at source.

The reason not to have reflexivity is because it is almost always leads to incoherency (in the formal sense, i.e a reasoner will entail unsatisfiable classes). This is the case for occurrent-part-of, which has range occurrent. Everything in the universe will be inferred to be part of an occurrent, including all continuants.

See the RO docs for more details.

To view this discussion on the web visit https://groups.google.com/d/msgid/bfo-discuss/CALGFikeb1x0J_B1nd9EzsVCsTBBJVbKhdsFzW6fEEPEofogxmg%40mail.gmail.com.

[Michael DeBellis]

I don't think making the reasoner too slow is ever a reason to remove an axiom from a reference ontology. 

I disagree. In fact I think this is a major problem with many reference ontologies and a peculiar view that some people have when building ontologies. If you developed a rule base or an object model and said "this is too slow to be used except with a few rows of data but it is a perfect model" people in those communities would look at you as if you were crazy. However with ontologies, I can't count the number of times I've tried to reuse a vocabulary ontology and found that it took forever to load because it was trying to model every possible aspect of reality rather than being a concise and reusable model for a specific domain, so I end up building my own rather than reusing.

IMO every reusable ontology should include a set of test data both to help developers understand how to use the ontology and to make sure that the ontology performs with reasonable speed. If you make a beautiful model but the reasoner is too slow even for medium amounts of data then what's the point? 

Also, I've seen many ontologies created by new users who add every possible axiom with the result being again that the reasoner takes forever to run with even moderate amounts of data (a few thousand or even hundred instances). IMO an axiom should only be added if there is some actual requirement that it satisfies. I wrote a blog article related to this recently: https://www.michaeldebellis.com/post/testing-and-debugging-ontologies 

Michael

To view this discussion on the web visit https://groups.google.com/d/msgid/bfo-discuss/CAN9AifvyBjsonOKwGFDtQ9hgRtf_khcJngKjtF1my0Mv5e6bLg%40mail.gmail.com.

[Chris Mungall]

Hi Michael

I appreciate the focus on users and utility here - this is something the upper ontology community needs to do more of!

However, it's very difficult to predict in advance which axioms might cause which problems. It's better for the source to be complete, and to provide different profiles for different use cases.

However, that said, ontologies can be authored in such a way that they are simpler for both humans and machines to reason over. For example, it's possible to have a complete theory of mereology using a non-reflexive part-of as primitive. While this is less mathematically elegant, it corresponds more to ordinary domain scientists' conception of their domain, and it turns out to be far more pragmatic in engineering terms.

Great blog article - I also have a series on testing and debugging:

https://douroucouli.wordpress.com/2018/08/03/debugging-ontologies-using-owl-reasoning-part-1-basics-and-disjoint-classes-axioms/

https://douroucouli.wordpress.com/2018/09/04/debugging-ontologies-using-owl-reasoning-part-2-unintentional-entailed-equivalence/

https://douroucouli.wordpress.com/2021/08/25/debugging-ontologies-using-owl-reasoning-part-3-robot-explain/

To view this discussion on the web visit https://groups.google.com/d/msgid/bfo-discuss/CALGFikca0xy%2ByPoOrSBx9QPKkeJnUquiOxN3aHiCaOKaGmoikw%40mail.gmail.com.

[Alan Ruttenberg]

From the readme at https://github.com/BFO-ontology/BFO-2020/tree/master/21838-2/owl

NOTE: The OWL is an approximation to the FOL theory, which is stronger. As an approximation it is incomplete, not only wrt. to the FOL, but also in the sense that there are potentially provably true OWL axioms that are not part of this version of the OWL. The BFO specification says that any and only OWL axioms that are provable from the FOL are valid for BFO OWL. It is intended that OWL file will become more complete over time. Feel free to add FOL provable OWL axioms to your version, and please submit an issue to https://github.com/BFO-ontology/BFO-2020/issues with them so they can be added to the distributed version.

On Sun, Aug 28, 2022 at 10:43 AM Stefan Schulz <ste...@gmail.com> wrote:

I am wondering why in the current OWL version of BFO 2020 

'occurrent part of' is not marked as "reflexive"

The FOL version has this. The OWL version has been "best effort". You can safely add it, and I would request that you submit a ticket so that it gets added to BFO OWL in a subsequent version.

According to the definition :

b 'proper occurrent part of' c =Def. 

    b 'occurrent part of' c & b and c are not identical [005-BFO]

the key difference between 

'occurrent part of' and  'proper occurrent part of' 

is exactly the reflexivity feature.  

I also do not understand why in the OWL version the former is marked as transitive and the latter isn't.  

It is provable in the FOL, so can be added to the OWL. Please submit a ticket.

All the OWL assertions are generated using (incomplete at the moment) heuristics and are then verified as provable from the FOL. For the OWL what would be needed is a check, for each relation and OWL property characteristic, whether the characteristic is provably the case. If you cite this email in the ticket I will endeavor to do that in a subsequent version.

Thanks,

Alan

Barry, Alan, could you explain?

Thanks!

Stefan

--

Stefan Schulz
Univ.-Prof. Dr. med.

Institute for Medical lnformatics, Statistics and Documentation
Medical University of Graz, Auenbruggerplatz 2/5
A-8036 Graz, Austria
Tel: +43 316 385 16939   |   +43 699 150 96 270  

Email:  stefan...@medunigraz.at
Web:   www.medunigraz.at/imi/  |  purl.org/steschu

[Stefan Schulz]

Chris, Michael,

The reason not to have reflexivity is because it is almost always leads to incoherency (in the formal sense, i.e a reasoner will entail unsatisfiable classes). This is the case for occurrent-part-of, which has range occurrent. Everything in the universe will be inferred to be part of an occurrent, including all continuants.

In my small ontology attached, the inferences are computed as expected only if I leave domain and range unconstrained. As soon as I add bfo:occurrent as domain and range constraints, exactly what you describe, happens (with ELK and HERMIT). 

Can you provide a logical explanation for this? 

--

Stefan 

 

--

Stefan Schulz
Univ.-Prof. Dr. med.

Institute for Medical lnformatics, Statistics and Documentation
Medical University of Graz, Auenbruggerplatz 2/5
A-8036 Graz, Austria
Tel: +43 316 385 16939   |   +43 699 150 96 270  

Email:  stefan...@medunigraz.at
Web:   www.medunigraz.at/imi/  |  purl.org/steschu

 

[Alan Ruttenberg]

Yes, thanks. Forgot about that. The reflexivity is qualified in the FOL

  (cl:comment "occurrent-part-of is reflexive [hbj-1]"
    (forall (a)
     (if (exists (t) (instance-of a occurrent t))
      (occurrent-part-of a a))))

Chris' suggested pattern works but can easily lead to violations of the global restrictions. It's been a while since I did work on BFO-2020 so I don't recall whether it triggers that with BFO-2020, but it's easy enough to try. Whether or not you are able to add it to your own ontology would depend on whether it lands up violating a global restriction.

Alan

To view this discussion on the web visit https://groups.google.com/d/msgid/bfo-discuss/CAN9AifscVndTSEDwhvoNTCB0Qknbe%3Dgi%3DuN04bDbf58U%3DrA4eA%40mail.gmail.com.

[Alan Ruttenberg]

Try making occurrent-part-of reflexive in the full BFO. You will see that all the classes in the continuant hierarchy become unsat.

You could add that proper-occurrent-part-of is irreflexive.

Alan

--

You received this message because you are subscribed to the Google Groups "BFO Discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to bfo-discuss...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/bfo-discuss/CAHM_EAt%3DHVSUwLPx7A%2B-X3XaVY7ZCqn51VmTO8miNeDt6WWKaw%40mail.gmail.com.

[Stefan Schulz]

Dear all, again, 

Am Mo., 29. Aug. 2022 um 19:37 Uhr schrieb Stefan Schulz <ste...@gmail.com>:

Chris, Michael,

The reason not to have reflexivity is because it is almost always leads to incoherency (in the formal sense, i.e a reasoner will entail unsatisfiable classes). This is the case for occurrent-part-of, which has range occurrent. Everything in the universe will be inferred to be part of an occurrent, including all continuants.

In my small ontology attached, the inferences are computed as expected only if I leave domain and range unconstrained. As soon as I add bfo:occurrent as domain and range constraints, exactly what you describe, happens (with ELK and HERMIT). 

Can you provide a logical explanation for this? 

I think I found and explanation in:

https://aifb.kit.edu/images/1/19/DL-Intro.pdf 

Reflexive: bfo:has_occurrent_part 

is the same as 

owl:Thing subclassOf bfo:has_occurrent_part some Self

... what explains the behaviour. 

But then, transitivity restricted to bfo:occurrent could be expressed by the axiom:

bfo:occurrent subclassOf bfo:has_occurrent_part some Self

Unfortunately, this is not supported by the reasoners I tried (HermiT, ELK, Fact++)

--

Stefan

  

[Stefan Schulz]

Alan, 

in the BFO2022 version I downloaded, proper_occurrent_part_of is not transitive. What is the reason for it?

-

Stefan

To view this discussion on the web visit https://groups.google.com/d/msgid/bfo-discuss/CAFKQJ8nhrxV5byFLabMrLcTdxj3b9CzSoGc9jfMNgRLTkYjQCg%40mail.gmail.com.

[Alan Ruttenberg]

Here is an example of using ObjectHasSelf for local reflexivity. c,o for continuant, occurrent. c1,o1 instances respectively. opo like occurrent-part-of. self-o the extra property needed, which is otherwise not to be used. You will see that it is inferred that :o1 :opo :o1, but not :c1 :opo :c1.

Prefix(:=<http://example.com/>)
Ontology(:lr
SubObjectPropertyOf(:self-o :opo)
EquivalentClasses(:o ObjectHasSelf(:self-o))
DisjointClasses(:o :c)
ClassAssertion(:o :o1)
ClassAssertion(:c :c1)
)

To view this discussion on the web visit https://groups.google.com/d/msgid/bfo-discuss/CAHM_EAtgHrS6-Nc9dAke5OjidAiVJDBSG6iVz9f_6frSoPDJVQ%40mail.gmail.com.

[Michael DeBellis]

Attached is a sample ontology I just built in Protege. It has two classes: Foo and Bar and one property hasFoo defined as Reflexive with domain and range Foo. When I create instances of Foo, Bar, and Thing (Foo1, Bar1, and Thing1) and then run the Pellet reasoner it asserts that Foo1, Bar1, and Thing1 hasFoo Foo1 Bar1 and Thing1 respectively. If I define Foo and Bar to be disjoint then I get an error from the Pellet reasoner. Also, the reasoner infers that Thing1 is an instance of Foo (because in spite of what is defined the actual domain and range of hasFoo are Thing and the reasoner has inferred that Foo and Thing are equivalent). You can also see this in the Class hierarchy (inferred) View, where Thing and Foo are equivalent and Bar is a subclass of Thing/Foo:

To view this discussion on the web visit https://groups.google.com/d/msgid/bfo-discuss/CAFKQJ8n9x5hmj2W6AYERrkTOHGY4sj_W2z_46MY61EHBgjNkQA%40mail.gmail.com.