Combinable Extensions of Abelian Groups

DOI10.1007/978-3-642-02959-2_4zbMath1250.03021OpenAlexW1500141485MaRDI QIDQ5191096

Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch

Publication date: 28 July 2009

Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_4

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Abelian groups (20K99) Quantifier elimination, model completeness, and related topics (03C10)

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 ⋮ Politeness and combination methods for theories with bridging functions ⋮ Model completeness, covers and superposition ⋮ Data Structures with Arithmetic Constraints: A Non-disjoint Combination

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• Superposition theorem proving for abelian groups represented as integer modules
• A rewriting approach to satisfiability procedures.
• Superposition with completely built-in abelian groups
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• Unification in the union of disjoint equational theories: Combining decision procedures
• Engineering DPLL(T) + Saturation
• Integrating Linear Arithmetic into Superposition Calculus
• ${\mathcal{T}}$ -Decision by Decomposition
• Automatic Decidability and Combinability Revisited
• Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
• Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
• Simplification by Cooperating Decision Procedures
• Complete Sets of Reductions for Some Equational Theories
• A comprehensive combination framework
• New results on rewrite-based satisfiability procedures
• Model-completions and modules