In the context of combinations of theories with disjoint signatures, we classify the component theories according to the decidability of constraint satisfiability problems in finite and 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 U 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 finite or infinite models, is decidable. We show that this result covers decision procedures based on rewriting, generalizing 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

BONACINA, Maria Paola;
2006-01-01

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 finite and 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 U 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 finite or infinite models, is decidable. We show that this result covers decision procedures based on rewriting, generalizing recent work on combination of theories in the rewrite-based approach to satisfiability.
2006
9783540371878
Decision procedures; combination; Nelson-Oppen schema; superposition; rewriting; deduction
File in questo prodotto:
File Dimensione Formato  
IJCAR2006rewsat+csp.pdf

accesso aperto

Descrizione: Articolo
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 398.83 kB
Formato Adobe PDF
398.83 kB Adobe PDF Visualizza/Apri

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: https://hdl.handle.net/11562/29913
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 34
  • ???jsp.display-item.citation.isi??? 25
social impact