Reasoning about taxonomies in first-order logic

Experts often disagree about the organization of biological taxa. The shifting definitions of taxonomic names complicate otherwise simple queries concerning these taxa. For example, a query such as "how many occurrences of specimens in genus G are recorded in database D" will return different answers depending on whose definition of genus G is used. In our proposed framework, taxonomic classifications of multiple experts are captured using first-order logic (FOL). Specifically, taxonomies, and relationships between them, are viewed as sets of first-order formulas, constraining the possible interpretations of names and concepts in the taxonomies. The formalization of taxonomies and the relationships between them via our FOL language L_tax allows us to clarify (a) what it means for a taxonomy to be consistent, (b) to be inconsistent, (c) whether a new relationship between two taxa (e.g., a congruence A ≡ B) is implied, thus "filling logic gaps", and (d) whether two taxonomies from different authorities, together with a taxonomy mapping (articulation) from a third authority, are mutually consistent. We illustrate our logic-based formalization and the resulting opportunities for automated reasoning support for biological taxonomies using examples involving the classification of a genus of plants. We elaborate on (a-d) above and give some example derivations in logic. We also show that while reasoning in L_tax is decidable, it might still be computationally hard (e.g., NP-complete) and thus infeasible over large taxonomies and articulations. By employing results from the spatial algebra RCC-5, we identify an important class of efficient taxonomy articulations, i.e., whose satisfiability can be checked in polynomial time.