Model-theoretic methods in combined constraint satisfiability

DOI10.1007/s10817-004-6241-5zbMath1069.03008OpenAlexW2082963442MaRDI QIDQ556677

Silvio Ghilardi

Publication date: 22 June 2005

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

Full work available at URL: https://doi.org/10.1007/s10817-004-6241-5

zbMATH Keywords

quantifier eliminationfusioncombinationcombined decidabilitymodel completionsNelson-Oppen proceduresuperposition calculus

Mathematics Subject Classification ID

Related Items (30)

Modular Termination and Combinability for Superposition Modulo Counter Arithmetic ⋮ Satisfiability Modulo Theories ⋮ A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited ⋮ Modularity results for interpolation, amalgamation and superamalgamation ⋮ Interpolation Results for Arrays with Length and MaxDiff ⋮ A Rewriting Approach to the Combination of Data Structures with Bridging Theories ⋮ On the verification of security-aware E-services ⋮ A new combination procedure for the word problem that generalizes fusion decidability results in modal logics ⋮ Modular proof systems for partial functions with Evans equality ⋮ Decision procedures for term algebras with integer constraints ⋮ A decidability result for the model checking of infinite-state systems ⋮ SMT-based verification of data-aware processes: a model-theoretic approach ⋮ Decision procedures for extensions of the theory of arrays ⋮ Interpolation and amalgamation for arrays with MaxDiff ⋮ Quantifier-free interpolation in combinations of equality interpolating theories ⋮ On Combinations of Local Theory Extensions ⋮ On Hierarchical Reasoning in Combinations of Theories ⋮ Unnamed Item ⋮ Ground Interpolation for the Theory of Equality ⋮ 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 ⋮ On Interpolation and Symbol Elimination in Theory Extensions ⋮ Model completeness, covers and superposition ⋮ Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis ⋮ Data Structures with Arithmetic Constraints: A Non-disjoint Combination ⋮ Combining Theories with Shared Set Operations ⋮ Combination of uniform interpolants via Beth definability ⋮ Combined covers and Beth definability ⋮ Applications of Hierarchical Reasoning in the Verification of Complex Systems

Uses Software

• SPASS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The complexity of linear problems in fields
• Complexity, convexity and combinations of theories
• Model theory.
• A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
• Model-companions and definability in existentially complete structures
• The computational complexity of logical theories
• Combining word problems through rewriting in categories with products
• Deciding the word problem in the union of equational theories.
• Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
• A general setting for flexibly combining and augmenting decision procedures
• Cooperation of background reasoners in theory reasoning by residue sharing
• Unions of non-disjoint theories and combinations of satisfiability procedures
• Simplification by Cooperating Decision Procedures
• Reasoning About Recursively Defined Data Structures
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Term Rewriting and All That
• Combining Non-Stably Infinite Theories
• Automated Reasoning

This page was built for publication: Model-theoretic methods in combined constraint satisfiability