Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures

Abstract. In the context of combinations of theories with disjoint signatures, we classify the component theories according to the decidability of constraint satisability problems in arbitrary and in innite models, respectively. We exhibit a theory T1 such that satisability is decidable, but satisability in innite models is undecidable. It follows that satisability in T1 T2 is undecidable, whenever T2 has only innite models, even if signatures are disjoint and satisability in T2 is 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 satisability problem, in either arbitrary or innite 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 satisability.

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
• Keywords: Automated Reasoning, CADE 2006, Constraint Satisability Problems, Innite Models, Nelson-Oppen Decidability Transfer