Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator

DOI10.3233/FI-2010-362zbMath1215.03051OpenAlexW1501719149MaRDI QIDQ3084983

Enrica Nicolini, Michaël Rusinowitch, Christophe Ringeissen

Publication date: 28 March 2011

Published in: Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3233/fi-2010-362

zbMATH Keywords

data structuresdecidabilityequational reasoningarithmetic constraintsinteger offsetssatisfiability procedureunion of non-disjoint theories

Mathematics Subject Classification ID

Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Data structures (68P05)

Related Items

Modular Termination and Combinability for Superposition Modulo Counter Arithmetic ⋮ A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited ⋮ Modularity results for interpolation, amalgamation and superamalgamation ⋮ A Rewriting Approach to the Combination of Data Structures with Bridging Theories ⋮ SMT-based verification of data-aware processes: a model-theoretic approach ⋮ Satisfiability Procedures for Combination of Theories Sharing Integer Offsets ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Politeness and combination methods for theories with bridging functions ⋮ Model completeness, covers and superposition