Reasoning about taxonomies in first-order logic

David Thau, Bertram Ludäscher

Research output: Contribution to journalArticlepeer-review


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 Ltax 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 Ltax 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.

Original languageEnglish (US)
Pages (from-to)195-209
Number of pages15
JournalEcological Informatics
Issue number3 SPEC. ISS.
StatePublished - Oct 2007
Externally publishedYes


  • Automated deduction (reasoning)
  • First-order logic constraints
  • Taxonomy

ASJC Scopus subject areas

  • Ecology, Evolution, Behavior and Systematics
  • Ecology
  • Modeling and Simulation
  • Ecological Modeling
  • Computer Science Applications
  • Computational Theory and Mathematics
  • Applied Mathematics


Dive into the research topics of 'Reasoning about taxonomies in first-order logic'. Together they form a unique fingerprint.

Cite this