Reasoning about taxonomies in first-order logic☆ Export

@article{citeulike:4017018, abstract = {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 inlMMLBox 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 inlMMLBox 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.}, author = {Thau, D. and Ludascher, B.}, citeulike-article-id = {4017018}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/j.ecoinf.2007.07.005}, citeulike-linkout-1 = {http://linkinghub.elsevier.com/retrieve/pii/S1574954107000489}, doi = {10.1016/j.ecoinf.2007.07.005}, issn = {15749541}, journal = {Ecological Informatics}, keywords = {reasoner, related-work}, month = {October}, number = {3}, pages = {195--209}, posted-at = {2009-02-06 17:57:49}, priority = {0}, title = {Reasoning about taxonomies in first-order logic☆}, url = {http://dx.doi.org/10.1016/j.ecoinf.2007.07.005}, volume = {2}, year = {2007} }

TY - JOUR ID - citeulike:4017018 L3 - citeulike-article-id:4017018 N2 - 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 inlMMLBox 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 inlMMLBox 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. IS - 3 JF - Ecological Informatics SN - 15749541 EP - 209 TI - Reasoning about taxonomies in first-order logic☆ VL - 2 SP - 195 KW - reasoner KW - related-work AU - Thau, D AU - Ludascher, B PY - 2007/10// UR - http://dx.doi.org/10.1016/j.ecoinf.2007.07.005 ER -