documentation/standards for defining axioms

[wdduncan]

I've seen a number of issues that mention guidance for writing axioms. E.g. (to name a few):

• Should we add seasons? #253
• Add and correct logical axioms to environmental zone #718
• Mixture terms require new imports #1006
• design patterns for emission processes #1039

Think we might want some documentation provide guidance. Themes I see in the tickets:

• Don't use complex subclass axioms (e.g., X and (part of some Y) and (located in some Z). Instead list the list each subclass axiom individually.
• Stick to with axioms that ELK can use for inference. I think ELK cannot use the following (but my list may be incomplete):
  • distinct individuals
  • same individuals
  • min/max cardinality
  • disjoint classes
  • data property assertions
• We may also need guidance on modeling complements (e.g., not part of some X)

[cmungall]

Don't use complex subclass axioms (e.g., X and (part of some Y) and (located in some Z). Instead list the list each subclass axiom individually.

Yes. Hopefully this is uncontroversial

Stick to with axioms that ELK can use for inference.

I would not put it exactly this way. Ontologies should state the axioms they need to state in order to support their use cases.

However, I make the following recommendation:

Avoid Complex Boolean Constructs and difficult to understand expressions

The primary motivation here is NOT to keep things simple for reasoners, it is to keep things simple for humans (having things be blazing fast for reasoning is a nice bonus)

I have seen again and again when OWL constructs such as ONLY, NOT, or deeply nested expressions are used (and even OR), mistakes are made. Many of these mistakes are cryptic - the axiom says something different than what the author intended. It also makes it harder for other people to help maintain your ontology. Even for experienced OWL developers, it's hard to mentally reason about certain constructs, so always best to keep it simple.

When it is necessary to use other constructs, there are patterns like EL-shunt to isolate them

I need to document these patterns and anti-patterns more. I will make a blog post on this but for now see the section OntoTip: Avoid Complex Boolean Constructs and difficult to understand expressions

[kaiiam]

I think this should be folded into the larger ENVO documentation work see discussion in our Working ENVO documentation.

[wdduncan]

I suggest we finish the current document before engaging on this. I posted the ticket in hopes of it not getting lost :)

[kaiiam]

Fair enough but I think something like this needs to be one of our doc pages.

[wdduncan]

@kaiiam Of course it does :)

[pbuttigieg]

Unless this is all in clear documentation (not a paper, not a textbook, not a blog post) on this tracker, it's all academic.

Stick to with axioms that ELK can use for inference. I think ELK cannot use the following (but my list may be incomplete):

The limits of a given reasoner are not of interest - we want to express the semantics the best way we can.

Don't use complex subclass axioms (e.g., X and (part of some Y) and (located in some Z). Instead list the list each subclass axiom individually.

As long as the end result is equivalent, sure, but I'm not sure this is always the case.

As noted above, we'll develop that section in the documentation draft we have going and then create a dedicated wiki page for it.

[wdduncan]

I only mentioned ELK as a way to test that the axioms are sufficiently simple and result in the inferences we want. Users may find it helpful to test inferences using ELK too, but I'm not tied to the idea. It was meant as a heuristic.

I'm fine with starting a doc, but let's finish the current one first, please.

[pbuttigieg]

I'm fine with starting a doc, but let's finish the current one first, please.

I think @kaiiam's doc is all inclusive, so maybe just adding a section for this would suffice?

[kaiiam]

Recaping what I think it's @cmungall's position it's better to have simpler but consistent axioms preferable following patterns. Hence avoiding NOT, ONLY etc. I think we should have a section about using DOSDPs and how to setup new ones based on an agreed upon design pattern.

This is maybe not as urgent so perhaps for now we just have a doc to explain the DOSDPs we do have the patterns they follow and how to use them?