Unions of non-disjoint theories and combinations of satisfiability procedures
From MaRDI portal
Publication:1853591
DOI10.1016/S0304-3975(01)00332-2zbMath1018.68033MaRDI QIDQ1853591
Christophe Ringeissen, Cesare Tinelli
Publication date: 21 January 2003
Published in: Theoretical Computer Science (Search for Journal in Brave)
decision problemsautomated deductionconstraint-based reasoningcombination of satisfiability procedures
Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
Combining Theories: The Ackerman and Guarded Fragments ⋮ Satisfiability Modulo Theories ⋮ A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited ⋮ Combining nonstably infinite theories ⋮ Deciding the word problem in the union of equational theories. ⋮ A Rewriting Approach to the Combination of Data Structures with Bridging Theories ⋮ A new combination procedure for the word problem that generalizes fusion decidability results in modal logics ⋮ Efficient theory combination via Boolean search ⋮ Decision procedures for term algebras with integer constraints ⋮ A decidability result for the model checking of infinite-state systems ⋮ Quantifier Elimination and Provers Integration ⋮ Combining Non-Stably Infinite Theories ⋮ Canonization for disjoint unions of theories ⋮ Model-theoretic methods in combined constraint satisfiability ⋮ On Hierarchical Reasoning in Combinations of Theories ⋮ Unnamed Item ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Politeness and combination methods for theories with bridging functions ⋮ Tractable combinations of theories via sampling ⋮ A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method ⋮ Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis ⋮ Combinations of Theories for Decidable Fragments of First-Order Logic ⋮ Combining Theories with Shared Set Operations ⋮ Combination of convex theories: modularity, deduction completeness, and explanation ⋮ Unions of non-disjoint theories and combinations of satisfiability procedures ⋮ Combining sets with cardinals
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unification in a combination of arbitrary disjoint equational theories
- On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems
- Combination techniques and decision problems for disunification
- Combination of constraint solvers for free and quasi-free structures
- Complexity, convexity and combinations of theories
- Combining matching algorithms: The regular case
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- A resolution principle for constrained logics
- Combining unification algorithms
- Combining symbolic constraint solvers on algebraic domains
- Combining word problems through rewriting in categories with products
- Deciding the word problem in the union of equational theories.
- Constraint contextual rewriting.
- Unions of non-disjoint theories and combinations of satisfiability procedures
- An introduction to fusion of strongly minimal sets: The geometry of fusions
- Modular properties of composable term rewriting systems
- Combining decision algorithms for matching in the union of disjoint equational theories
- Unification in the union of disjoint equational theories: Combining decision procedures
- Deciding Combinations of Theories
- Completion of a Set of Rules Modulo a Set of Equations
- Simplification by Cooperating Decision Procedures
- A Practical Decision Procedure for Arithmetic with Function Symbols
- Amalgamations preserving ℵ1-categoricity
- Combination techniques for non-disjoint equational theories
- A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
- Combination of constraint systems II: Rational amalgamation
