Title
Phylogenetic incongruence through the lens of Monadic Second Order logic.
Abstract
Within the field of phylogenetics there is growing interest in measures for summarising the dissimilarity, or 'incongruence', of two or more phylogenetic trees. Many of these measures are NP-hard to compute and this has stimulated a considerable volume of research into fixed parameter tractable algorithms. In this article we use Monadic Second Order logic (MSOL) to give alternative, compact proofs of fixed parameter tractability for several well-known incongruency measures. In doing so we wish to demonstrate the considerable potential of MSOL - machinery still largely unknown outside the algorithmic graph theory community - within phylogenetics. A crucial component of this work is the observation that many of these measures, when bounded, imply the existence of an 'agreement forest' of bounded size, which in turn implies that an auxiliary graph structure, the display graph, has bounded treewidth. It is this bound on treewidth that makes the machinery of MSOL available for proving fixed parameter tractability. We give a variety of different MSOL formulations. Some are based on explicitly encoding agreement forests, while some only use them implicitly to generate the treewidth bound. Our formulations introduce a number of "phylogenetics MSOL primitives" which will hopefully be of use to other researchers.
Year
DOI
Venue
2016
10.7155/jgaa.00390
J. Graph Algorithms Appl.
Field
DocType
Volume
Graph,Discrete mathematics,Combinatorics,Phylogenetic tree,Algorithmic graph theory,Monadic second-order logic,Mathematical proof,Through-the-lens metering,Treewidth,Mathematics,Bounded function
Journal
20
Issue
Citations 
PageRank 
2
3
0.40
References 
Authors
12
4
Name
Order
Citations
PageRank
Steven Kelk119325.60
Leo van Iersel221524.58
Celine Scornavacca3263.73
Mathias Weller430.40