具有直接失配约束的单元浅层线性一阶片段的可判定性
计算机科学中的逻辑
2017-05-25 v2
摘要
单元浅层线性 Horn 片段广为人知是可判定的，并具有许多应用，例如在安全协议分析、树自动机或抽象精化中。如何将该片段扩展到非 Horn 情形并保持可判定性，例如使其能够表达协议中的非确定性，一直是一个长期悬而未决的问题。我们通过有序消解并进一步扩展以失配约束，证明了非 Horn 单元浅层线性片段的可判定性，并讨论了这一新可判定片段的一些应用。
引用
@article{arxiv.1703.02837,
title = {Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints},
author = {Andreas Teucke and Christoph Weidenbach},
journal= {arXiv preprint arXiv:1703.02837},
year = {2017}
}
备注
29 pages, long version of CADE-26 paper