关于未解释一元谓词的实数差分逻辑的可判定性
摘要：限量化、算术和无解释谓词混合的一阶逻辑片断通常是不可判定的，例如，将Presburger算术与一个无解释的一元谓词扩展。在SMT世界中，差分逻辑是线性算术的一种非常受欢迎的片断，比Presburger算术的表达能力更低。已知整数上的差分逻辑与无解释的一元谓词在量词的存在下是可判定的。我们在这里惊讶地展示，对于具有单个无解释的一元谓词的实数上的（限量化的）差分逻辑是不可判定的。此外，我们证明整数上的差分逻辑与实数上的顺序结合无解释的一元谓词仍然是可判定的。
作者：Bernard Boigelot (1), Pascal Fontaine (1), Baptiste Vergain (1) ((1) Montefiore Institute, Universit''e de Li`ege, Belgium)
论文ID：2305.15059
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-05-25