Should we explicitly identify terminal nodes in the OWL output?

[gaurav]

CDAO has a TerminalNode class defined as Node and (has_Child only not ()). However, this can't resolve under an open-world assumption, since we don't know that any terminal node in our phylogeny doesn't have a child node we don't know about. Should we explicitly mark terminal nodes as TerminalNodes in the phylo2owl output?

[hlapp]

What makes you think it cannot resolve? Universal quantifications certainly can resolve, because their truth can be asserted for any particular individual (or for a class of individuals). So yes, simply asserting a node to be an instance of TerminalNode is a fine way of doing this if the purpose isn't to have membership in this class be determined dynamically by way of reasoning. Which, if we are converting a given instance of a phylogeny, indeed isn't the purpose.

Having said that, more generally speaking there are axioms in CDAO that are both seldom needed in practice and harmful for practical reasoning, because they require the full OWL-DL expressivity profile, or one that is more complex than EL, which rules out some reasoners (such as ELK) that would otherwise be very fast. So there's the separate issue here that we'll need to separate CDAO into a "core" that ideally could be kept to OWL-EL, and "CDAO-full" that will need a DL reasoner.

[gaurav]

Maybe I should have said that it doesn't resolve, in that Node and (has_Child only (not (Node))) doesn't match any Nodes in FacT++ and HermiT on Protege.

Is there any downside to asserting those classes in the ontologies generated by phylo2owl? That might make it easier to identify the roots of the phylogenies, which would be useful!