Deciding Combinations of Theories
From MaRDI portal
Recommendations
Cited in
(60)- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Combination of convex theories: modularity, deduction completeness, and explanation
- Application of conditional term substitution systems in program verification
- Unification in combinations of collapse-free regular theories
- A rewriting approach to satisfiability procedures.
- Constraint contextual rewriting.
- Algorithms and reductions for rewriting problems. II.
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Unification modulo lists with reverse relation with certain word equations
- Strategies for combining decision procedures
- Metalevel algorithms for variant satisfiability
- Efficient theory combination via Boolean search
- A taxonomy of exact methods for partial Max-SAT
- Being careful about theory combination
- Partition-based logical reasoning for first-order and propositional theories
- Canonization for disjoint unions of theories
- A randomized satisfiability procedure for arithmetic and uninterpreted function symbols
- Embedded software verification using symbolic execution and uninterpreted functions
- Complexity assessments for decidable fragments of Set Theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages
- Combining WS1S and HOL
- Order-Sorted Rewriting and Congruence Closure
- Metalevel algorithms for variant satisfiability
- Combining SAT methods with non-clausal decision heuristics
- Model-based theory combination
- \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
- Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
- Deciding Extensions of the Theories of Vectors and Bags
- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
- Data structures with arithmetic constraints: A non-disjoint combination
- scientific article; zbMATH DE number 3898849 (Why is no real title available?)
- scientific article; zbMATH DE number 4043224 (Why is no real title available?)
- scientific article; zbMATH DE number 1302382 (Why is no real title available?)
- Combining decision procedures by (model-)equality propagation
- On quasitautologies
- On Shostak's decision procedure for combinations of theories
- Variant-Based Satisfiability in Initial Algebras
- scientific article; zbMATH DE number 2090060 (Why is no real title available?)
- scientific article; zbMATH DE number 2090127 (Why is no real title available?)
- scientific article; zbMATH DE number 2090312 (Why is no real title available?)
- Solving constraint satisfaction problems with SAT modulo theories
- Uniform interpolants in \(\mathcal{EUF}\): algorithms using DAG-representations
- Painless programming combining reduction and search, design principles for embedding decision procedures in high-level languages
- Combining Decision Procedures by (Model-)Equality Propagation
- Combinable Extensions of Abelian Groups
- A practical integration of first-order reasoning and decision procedures
- Connecting many-sorted theories
- Combining decision procedures for the reals
- Cover Algorithms and Their Combination
- Automatic decidability and combinability
- Unification in Boolean rings and Abelian groups
- CONCUR 2005 – Concurrency Theory
- FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
- Unification in a combination of equational theories: an efficient algorithm
- KBO Constraint Solving Revisited
- Computing ground congruence classes
- Producing and verifying extremely large propositional refutations
- Theory exploration powered by deductive synthesis
- FTP'2003: 4th international workshop on first-order theorem proving. Proceedings of the workshop (in connection with RDP'03, federated conference on rewriting, deduction and programming), Valencia, Spain, June 12--14, 2003
This page was built for publication: Deciding Combinations of Theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3766889)
