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

DOI10.1007/11814771_42zbMath1222.03011OpenAlexW1543051890MaRDI QIDQ3613431

Maria Paola Bonacina, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli, Silvio Ghilardi

Publication date: 12 March 2009

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.138.8496

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items (11)

On deciding satisfiability by theorem proving with speculative inferences ⋮ A decidability result for the model checking of infinite-state systems ⋮ An instantiation scheme for satisfiability modulo theories ⋮ Decision procedures for extensions of the theory of arrays ⋮ Superposition for Bounded Domains ⋮ Automatic decidability and combinability ⋮ On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving ⋮ Combinable Extensions of Abelian Groups ⋮ Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis ⋮ Theory decision by decomposition ⋮ Combination of convex theories: modularity, deduction completeness, and explanation

Uses Software

• E Theorem Prover

This page was built for publication: Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures