一元二阶逻辑视角下的系统发生不一致
Phylogenetic incongruence through the lens of Monadic Second Order logic
摘要：
在遗传学领域内，人们对总结两个或多个系统发育树的相异或“不一致”的措施越来越感兴趣。许多这些措施是NP难计算，这刺激了相当数量的研究固定参数听话的算法。在这篇文章中，我们使用一元二阶逻辑（MSOL）给出替代，紧凑的证明固定参数易处理的几个著名的不一致性措施。在这样做的时候，我们希望证明MSOL的巨大潜力-机器仍然在很大程度上未知的算法图论社区以外-在遗传学。这项工作的一个重要组成部分是观察到，许多这些措施，有界时，意味着存在一个“协议森林”的有界大小，这反过来又意味着一个辅助图结构，显示图，有界树宽。正是树宽上的这个界使得MSOL的机器可用于证明固定参数的易处理性。我们给出了各种不同的MSOL配方。有些基于显式编码协议林，而有些仅隐式使用它们来生成树宽界限。我们的配方介绍了一些“遗传学MSOL原语”，这将有望被用于其他研究人员。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
