VoCamp1/Monophyly in DL
Can one express monophyly conveniently in OWL-DL, and use it in reasoning? Yes. See File:Monophyletic example.owl.txt.
The idea is to take taxa to be OWL classes whose members might be variously individual organisms or populations of organisms (at some time point). A class (taxon) is monophyletic if it is closed under descent and has a unique founder. In DL you can assert that a class is monophyletic by giving a name to its founding individual and equating the class with the class of descendents of that individual.
We start by defining a relation is-child-of that is inverse functional (this would argue for asexual reproduction, restriction to consideration of maternal or paternal contribution, or to the individuals being populations), and a relation is-descendent-of that is its reflexive transitive closure. To do this, assert that is-child-of is a subproperty of is-descendent-of, and assert that is-descendent-of is transitive and reflexive.
Now create a monophyletic taxon by creating a class and its founder individual and specifying that the class is equivalent to the (anonymous) class 'is-descendend-of value founder1' where founder1 is the founder.
For use in reasoning, consider the fact that the union of disjoint monophyletic classes cannot be monophyletic. If we set up this configuration - class A equal to the union of disjoint subclasses B and C, all of them equal to the descent closure of their respective founders - and run Fact++ to check for consistency, it tells us the ontology is inconsistent.