Complexity, convexity and combinations of theories

DOI10.1016/0304-3975(80)90059-6zbMath0437.03007OpenAlexW2072380992MaRDI QIDQ1141138

Derek C. Oppen

Publication date: 1980

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(80)90059-6

zbMATH Keywords

satisfiability problemarraysdisjunctive normal formintegerscomplexity of decidable combinations of theoriesdecidable quantifier-free theorieslist structureuninterpreted function symbols

Mathematics Subject Classification ID

Related Items (35)

Sharing Is Caring: Combination of Theories ⋮ Satisfiability Modulo Theories ⋮ Combining nonstably infinite theories ⋮ An institution-independent proof of the Robinson consistency theorem ⋮ Combination of constraint solvers for free and quasi-free structures ⋮ Metalevel algorithms for variant satisfiability ⋮ Horn Clause Solvers for Program Verification ⋮ Interpolation for predefined types ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ Efficient theory combination via Boolean search ⋮ Combining decision procedures by (model-)equality propagation ⋮ Complexity assessments for decidable fragments of Set Theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages ⋮ Being careful about theory combination ⋮ Many-sorted equivalence of shiny and strongly polite theories ⋮ Dynamic causes for the violation of timed reachability properties ⋮ Quantifier Elimination and Provers Integration ⋮ Combining Non-Stably Infinite Theories ⋮ Model-theoretic methods in combined constraint satisfiability ⋮ Unnamed Item ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ A semantic approach to interpolation ⋮ Order-Sorted Rewriting and Congruence Closure ⋮ Colors Make Theories Hard ⋮ Tractable combinations of theories via sampling ⋮ Metalevel Algorithms for Variant Satisfiability ⋮ 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 ⋮ Combining Equational Reasoning ⋮ Unions of non-disjoint theories and combinations of satisfiability procedures ⋮ Model-based Theory Combination ⋮ Generalised graded interpolation ⋮ Combining sets with cardinals ⋮ A tool for deciding the satisfiability of continuous-time metric temporal logic ⋮ Symbolic computation in Maude: some tapas

Cites Work

• Unnamed Item
• The complexity of logical theories
• A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
• Solvable cases of the decision problem
• Verification Decidability of Presburger Array Programs
• Fast Decision Procedures Based on Congruence Closure
• Simplification by Cooperating Decision Procedures
• Variations on the Common Subexpression Problem
• Khachiyan’s algorithm for linear programming
• Reasoning About Recursively Defined Data Structures
• A Practical Decision Procedure for Arithmetic with Function Symbols
• Bounds on Positive Integral Solutions of Linear Diophantine Equations
• An algorithm for reasoning about equality
• Assignment Commands with Array References
• Presburger arithmetic with bounded quantifier alternation
• Some Completeness Results in the Mathematical Theory of Computation

This page was built for publication: Complexity, convexity and combinations of theories