Model-theoretic methods in combined constraint satisfiability
From MaRDI portal
Publication:556677
DOI10.1007/S10817-004-6241-5zbMATH Open1069.03008OpenAlexW2082963442MaRDI QIDQ556677FDOQ556677
Authors: 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
Recommendations
combinationfusionquantifier eliminationcombined decidabilitymodel completionsNelson-Oppen proceduresuperposition calculus
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Quantifier elimination, model completeness, and related topics (03C10)
Cites Work
- Complexity, convexity and combinations of theories
- Simplification by Cooperating Decision Procedures
- Model theory.
- Term Rewriting and All That
- A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- The complexity of linear problems in fields
- Paramodulation-based theorem proving
- Title not available (Why is that?)
- Title not available (Why is that?)
- The computational complexity of logical theories
- Deciding the word problem in the union of equational theories.
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Title not available (Why is that?)
- Title not available (Why is that?)
- Model-companions and definability in existentially complete structures
- Combining word problems through rewriting in categories with products
- 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
- Solving numerical constraints
- Algebraic and model theoretic techniques for fusion decidability in modal logics
- Reasoning About Recursively Defined Data Structures
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Combining non-stably infinite theories
- Automated Reasoning
Cited In (46)
- Decision procedures for extensions of the theory of arrays
- On Hierarchical Reasoning in Combinations of Theories
- Frontiers of Combining Systems
- Modular termination and combinability for superposition modulo counter arithmetic
- Title not available (Why is that?)
- SMT-based verification of data-aware processes: a model-theoretic approach
- Interpolation and amalgamation for arrays with MaxDiff
- On the verification of security-aware E-services
- Title not available (Why is that?)
- Title not available (Why is that?)
- Tractable combinations of temporal CSPs
- A gentle non-disjoint combination of satisfiability procedures
- Automatic Combinability of Rewriting-Based Satisfiability Procedures
- Quantifier-free interpolation in combinations of equality interpolating theories
- A rewriting approach to the combination of data structures with bridging theories
- A decidability result for the model checking of infinite-state systems
- A polite non-disjoint combination method: theories with bridging functions revisited
- Politeness and combination methods for theories with bridging functions
- Combining non-stably infinite theories
- Combined covers and Beth definability
- Applications of hierarchical reasoning in the verification of complex systems
- On combinations of local theory extensions
- Modularity results for interpolation, amalgamation and superamalgamation
- Data structures with arithmetic constraints: A non-disjoint combination
- Combining theories with shared set operations
- Interpolation Results for Arrays with Length and MaxDiff
- Decision procedures for term algebras with integer constraints
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Satisfiability modulo theories
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes)
- Complexity of combinations of qualitative constraint satisfaction problems
- Combination of convex theories: modularity, deduction completeness, and explanation
- On the convexity of a fragment of pure set theory with applications within a Nelson-Oppen framework
- Model completeness, covers and superposition
- 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
- Logics in Artificial Intelligence
- Model-based theory combination
- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
- A comprehensive combination framework
- Noetherianity and Combination Problems
- Constraint solving for finite model finding in SMT solvers
- Combination of uniform interpolants via Beth definability
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Ground Interpolation for the Theory of Equality
Uses Software
This page was built for publication: Model-theoretic methods in combined constraint satisfiability
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q556677)
