Deciding Combinations of Theories
From MaRDI portal
Publication:3766889
DOI10.1145/2422.322411zbMath0629.68089OpenAlexW2030670832MaRDI QIDQ3766889
Publication date: 1984
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/2422.322411
program specificationprogram verificationdecision proceduresequational theoriescombinations of unquantified first-order theories
Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)
Related Items
Strategies for combining decision procedures, Unification in combinations of collapse-free regular theories, Metalevel algorithms for variant satisfiability, A rewriting approach to satisfiability procedures., Constraint contextual rewriting., Efficient theory combination via Boolean search, A taxonomy of exact methods for partial Max-SAT, Combining decision procedures by (model-)equality propagation, Complexity assessments for decidable fragments of Set Theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages, On quasitautologies, First-order automated reasoning with theories: when deduction modulo theory meets practice, Partition-based logical reasoning for first-order and propositional theories, Solving constraint satisfaction problems with SAT modulo theories, Canonized Rewriting and Ground AC Completion Modulo Shostak Theories, On Shostak's decision procedure for combinations of theories, Producing and verifying extremely large propositional refutations, Canonization for disjoint unions of theories, A randomized satisfiability procedure for arithmetic and uninterpreted function symbols, Combining Decision Procedures by (Model-)Equality Propagation, Unification in Boolean rings and Abelian groups, Unnamed Item, Variant-Based Satisfiability in Initial Algebras, Embedded software verification using symbolic execution and uninterpreted functions, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates, Satisfiability Procedures for Combination of Theories Sharing Integer Offsets, Order-Sorted Rewriting and Congruence Closure, Unification modulo lists with reverse relation with certain word equations, Metalevel Algorithms for Variant Satisfiability, A practical integration of first-order reasoning and decision procedures, Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis, Data Structures with Arithmetic Constraints: A Non-disjoint Combination, Combination of convex theories: modularity, deduction completeness, and explanation, Algorithms and reductions for rewriting problems. II., Unions of non-disjoint theories and combinations of satisfiability procedures, Model-based Theory Combination, CC(X): Semantic Combination of Congruence Closure with Solvable Theories
