Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
复制标题
Nelson-Oppen 和基于重写的决策程序的可判定性和不可判定性结果
DOI：
10.1007/11814771_42
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
D. Zucchelli
中科院分区：
文献类型：
--
作者：
M. P. Bonacina;S. Ghilardi;Enrica Nicolini;Silvio Ranise;D. Zucchelli
在理论与不相交签名的组合的背景下，我们分类的组件理论根据任意和无限模型中的约束可满足性问题的可判定性。我们证明了一个定理T1，使得可满足性是可判定的，但在无限模型中可满足性是不可判定的。在本文的第二部分中，我们加强了Nelson-Oppen可判定性转移的结果，证明了它适用于不相交签名理论，其可满足性问题在任意或无限模型下都是可判定的。我们发现，这一结果涵盖了基于重写的决策程序，补充了最近的工作结合理论的重写为基础的方法，以满足。
In the context of combinations of theories with disjoint signatures, we classify the component theories according to the decidability of constraint satisfiability problems in arbitrary and in infinite models, respectively. We exhibit a theoryT1such that satisfiability is decidable, but satisfiability in infinite models is undecidable. It follows that satisfiability inT1∪T2is undecidable, wheneverT2has only infinite models, even if signatures are disjoint and satisfiability inT2is decidable.In the second part of the paper we strengthen the Nelson-Oppen decidability transfer result, by showing that it applies to theories over disjoint signatures, whose satisfiability problem, in either arbitrary or infinite models, is decidable. We show that this result covers decision procedures based on rewriting, complementing recent work on combination of theories in the rewrite-based approach to satisfiability.