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 theory T 1 such that satisfiability is decidable, but satisfiability in infinite models is undecidable. It follows that satisfiability in T 1∪T 2 is undecidable, whenever T 2 has only infinite models, even if signatures are disjoint and satisfiability in T 2 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 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.

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

Ranise, Silvio;
2006

Abstract

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 theory T 1 such that satisfiability is decidable, but satisfiability in infinite models is undecidable. It follows that satisfiability in T 1∪T 2 is undecidable, whenever T 2 has only infinite models, even if signatures are disjoint and satisfiability in T 2 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 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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11582/22076
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact