Phylogenetic trees in ACL2

Biologists studying the evolutionary relationships between organisms use software packages to solve the computational problems they encounter. Several of these problems involve the production and analysis of phylogenetic trees. We present our system for phylogenetic tree manipulation, TASPI, which was designed to allow the specification and verification of various tree operations, while giving good execution performance. The first aspect of TASPI is a new format for storing and manipulating phylogenetic trees that significantly reduces storage requirements while continuing to allow the trees to be used as input to post-tree analysis. We also prove the correspondence of this format to another tree format. In addition, we give a consensus algorithm with verified guards that is faster by an order of magnitude than standard phylogenetic analysis tools. Categories and Subject Descriptors E.2 [Data Storage Representations]: Hash-table representations; F.4.1 [Mathematical Logic]: Mechan...

• Type: Conference
• Year: 2006
• Where: ACL2
• Authors: Warren A. Hunt Jr., Serita M. Nelesen
• Keywords: ACL2 2006, Computational Linguistics, Phylogenetic Tree Manipulation, Phylogenetic Trees, Standard Phylogenetic Analysis