Unions of non-disjoint theories and combinations of satisfiability procedures
From MaRDI portal
Publication:1853591
DOI10.1016/S0304-3975(01)00332-2zbMATH Open1018.68033MaRDI QIDQ1853591FDOQ1853591
Authors: Cesare Tinelli, Christophe Ringeissen 
Publication date: 21 January 2003
Published in: Theoretical Computer Science (Search for Journal in Brave)
Recommendations
automated deductiondecision problemsconstraint-based reasoningcombination of satisfiability procedures
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25)
Cites Work
- Title not available (Why is that?)
- Complexity, convexity and combinations of theories
- Simplification by Cooperating Decision Procedures
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Title not available (Why is that?)
- Unification in the union of disjoint equational theories: Combining decision procedures
- Title not available (Why is that?)
- Unification in a combination of arbitrary disjoint equational theories
- Title not available (Why is that?)
- Combining unification algorithms
- Combining symbolic constraint solvers on algebraic domains
- Modular properties of composable term rewriting systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Combination of constraint solvers for free and quasi-free structures
- Deciding the word problem in the union of equational theories.
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Deciding Combinations of Theories
- Title not available (Why is that?)
- On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems
- Completion of a Set of Rules Modulo a Set of Equations
- Title not available (Why is that?)
- Combining word problems through rewriting in categories with products
- Combining matching algorithms: The regular case
- Title not available (Why is that?)
- Combination techniques and decision problems for disunification
- Title not available (Why is that?)
- Combination techniques for non-disjoint equational theories
- Title not available (Why is that?)
- A resolution principle for constrained logics
- Combining decision algorithms for matching in the union of disjoint equational theories
- A Practical Decision Procedure for Arithmetic with Function Symbols
- Combination of constraint systems II: Rational amalgamation
- Amalgamations preserving ℵ1-categoricity
- Title not available (Why is that?)
- Constraint contextual rewriting.
- An introduction to fusion of strongly minimal sets: The geometry of fusions
- Title not available (Why is that?)
- A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
Cited In (47)
- On Hierarchical Reasoning in Combinations of Theories
- Frontiers of Combining Systems
- Canonization for disjoint unions of theories
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Efficient theory combination via Boolean search
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Combining Proof-Producing Decision Procedures
- Theoretical Aspects of Computing - ICTAC 2004
- Title not available (Why is that?)
- Title not available (Why is that?)
- Tractable combinations of temporal CSPs
- Model-theoretic methods in combined constraint satisfiability
- Combining theories: the Ackerman and guarded fragments
- A gentle non-disjoint combination of satisfiability procedures
- 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
- Theory combination: beyond equality sharing
- Combining nonstably infinite theories
- Conflict-driven satisfiability for theory combination: transition system and completeness
- Politeness and combination methods for theories with bridging functions
- Combination of disjoint theories: beyond decidability
- Combining non-stably infinite theories
- Deciding the word problem in the union of equational theories.
- Combining satisfiability procedures for unions of theories with a shared counting operator
- Data structures with arithmetic constraints: A non-disjoint combination
- Combining theories with shared set operations
- 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
- Tractable combinations of theories via sampling
- Unification in the union of disjoint equational theories: Combining decision procedures
- A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
- Combination of convex theories: modularity, deduction completeness, and explanation
- Cover Algorithms and Their Combination
- A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
- Satisfiability modulo theories and assignments
- Quantifier Elimination and Provers Integration
- Combining sets with cardinals
- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
- A comprehensive combination framework
- Computer Science Logic
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Combinations of Theories for Decidable Fragments of First-Order Logic
This page was built for publication: Unions of non-disjoint theories and combinations of satisfiability procedures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1853591)
