二阶逻辑的一个可判定片段及其在综合中的应用
计算机科学中的逻辑
2018-09-28 v3 编程语言
摘要
我们提出一种称为 EQSMT 的多类二阶逻辑片段,并证明该片段中句子的可满足性检查是可判定的。EQSMT 公式具有 量词前缀(作用于变量、函数与关系),使得 EQSMT 利于建模综合问题。此外,EQSMT 允许使用背景理论的结合推理,只要这些理论对 一阶片段具有可判定的可满足性问题(例如线性算术)。我们的判定过程将 EQSMT 公式的可满足性归约为各个背景理论的 公式的可满足性查询,从而使我们能够使用现有的支持 推理的高效 SMT 求解器;因此我们的过程可视为有效量化 SMT(EQSMT)推理。勘误:我们修改了变换步骤2(第9页)以修正一处轻微错误。此外,定理10上方的描述与发表版本不同。
引用
@article{arxiv.1712.05513,
title = {A Decidable Fragment of Second Order Logic With Applications to Synthesis},
author = {P. Madhusudan and Umang Mathur and Shambwaditya Saha and Mahesh Viswanathan},
journal= {arXiv preprint arXiv:1712.05513},
year = {2018}
}