| Authors: |
David Thau
and Bertram Ludascher
|
| URL: |
http://www.sciencedirect.com/science/article/B7W63-4PTN945-2/2/4cd391f1abf16ffdcc707977aabf855d |
| Description: |
ScienceDirect - Ecological Informatics : Reasoning about taxonomies in first-order logic |
| Tags: |
(reasoning)
Automated
First-order
Taxonomy
constraints
deduction
logic
|
| 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 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 [identical to] 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 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. |
@article{keyhere,
title = {Reasoning about taxonomies in first-order logic},
author = {David Thau and Bertram Ludascher},
booktitle = {Meta-information systems and ontologies. A Special Feature from the 5th International Conference on Ecological Informatics ISEI5, Santa Barbara, CA, Dec. 4-7, 2006 - Novel Concepts of Ecological Data Management S.I.},
journal = {Ecological Informatics},
month = {#oct#},
number = {3},
pages = {195--209},
url = {http://www.sciencedirect.com/science/article/B7W63-4PTN945-2/2/4cd391f1abf16ffdcc707977aabf855d},
volume = {2},
year = {2007},
description = {ScienceDirect - Ecological Informatics : Reasoning about taxonomies in first-order logic},
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 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 [identical to] 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 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.},
keywords = {(reasoning) Automated First-order Taxonomy constraints deduction logic }
}
::