自动机上的一阶量化
摘要：混合算术与未解释谓词的公式决策具有实际意义，尤其是在验证应用中。一些决策过程采用结构归纳构建能够识别待分析公式模型集合的自动机，然后测试该自动机是否接受非空语言。缺点是普遍量化通常通过减小成存在量化和求补来处理。对于模型被编码为无穷长字的逻辑形式而言，由于难以计算无穷长字自动机的补集，这个方法的实际应用受到了阻碍。本文的贡献是引入一种算法，直接计算一阶普遍量化符对识别模型集合的自动机的影响，针对采用一元表示法编码的自然数的公式。这使得可以应用基于自动机的方法获得可实现的各种算术理论的决策过程。
作者：Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
论文ID：2306.04210
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-08