Simplification by Cooperating Decision Procedures
From MaRDI portal
Publication:3899468
DOI10.1145/357073.357079zbMath0452.68013OpenAlexW2164778826MaRDI QIDQ3899468
Publication date: 1979
Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/357073.357079
Analysis of algorithms and problem complexity (68Q25) Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)
Related Items
Decision Procedures for Region Logic, Combining Theories: The Ackerman and Guarded Fragments, A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints, Sharing Is Caring: Combination of Theories, Modular Termination and Combinability for Superposition Modulo Counter Arithmetic, Satisfiability Modulo Theories, Combining Model Checking and Deduction, A Decision Procedure for (Co)datatypes in SMT Solvers, A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited, Modular higher-order E-unification, Combination of constraint solving techniques: An algebraic point of view, On the cooperation of the constraint domains ℋ, ℛ, and ℱ in CFLP, Satisfiability Checking: Theory and Applications, On First-Order Model-Based Reasoning, Optimization Modulo Theories with Linear Rational Costs, Interpolation for predefined types, Reasoning about vectors: satisfiability modulo a theory of sequences, Combining stable infiniteness and (strong) politeness, Deciding Theoremhood in Fibred Logics Without Shared Connectives, Analysis and Transformation of Constrained Horn Clauses for Program Verification, Improving complex SMT strategies with learning, Interpolation Results for Arrays with Length and MaxDiff, Variants and satisfiability in the infinitary unification wonderland, Towards a dereversibilizer: fewer asserts, statically, Verifying Heap-Manipulating Programs in an SMT Framework, Adapting Real Quantifier Elimination Methods for Conflict Set Computation, On quasitautologies, Modular Constraint Solver Cooperation via Abstract Interpretation, Canonized Rewriting and Ground AC Completion Modulo Shostak Theories, On Interpolation in Decision Procedures, On Shostak's decision procedure for combinations of theories, Quantifier-free interpolation in combinations of equality interpolating theories, On Combinations of Local Theory Extensions, Quantifier Elimination and Provers Integration, Combining Non-Stably Infinite Theories, Combining Decision Procedures by (Model-)Equality Propagation, Unnamed Item, On Hierarchical Reasoning in Combinations of Theories, On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving, Combinable Extensions of Abelian Groups, Unnamed Item, Unnamed Item, Variant-Based Satisfiability in Initial Algebras, Ground Interpolation for the Theory of Equality, Satisfiability Procedures for Combination of Theories Sharing Integer Offsets, Efficient Interpolant Generation in Satisfiability Modulo Theories, Unnamed Item, Decision Procedures for Automating Termination Proofs, Efficient Term-ITE Conversion for Satisfiability Modulo Theories, Modular SMT Proofs for Fast Reflexive Checking Inside Coq, A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method, Combining Equational Reasoning, Combinations of Theories for Decidable Fragments of First-Order Logic, Data Structures with Arithmetic Constraints: A Non-disjoint Combination, Combining Theories with Shared Set Operations, Distributing the Workload in a Lazy Theorem-Prover, A decision procedure for (co)datatypes in SMT solvers, Automated generation of exam sheets for automated deduction, Proof tree preserving tree interpolation, Interpolation systems for ground proofs in automated deduction: a survey, A heuristic prover for real inequalities, Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs, Strategies for combining decision procedures, An overview of the Tecton proof system, A decision procedure for combinations of propositional temporal logic and other specialized theories, A structure-preserving clause form translation, Modularity results for interpolation, amalgamation and superamalgamation, Unification in combinations of collapse-free regular theories, Embedding complex decision procedures inside an interactive theorem prover., Combining nonstably infinite theories, Deciding Boolean algebra with Presburger arithmetic, Rewriting modulo SMT and open system analysis, An institution-independent proof of the Robinson consistency theorem, Solving linear optimization over arithmetic constraint formula, Combination of constraint solvers for free and quasi-free structures, Structured proof procedures, Metalevel algorithms for variant satisfiability, An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty, Complexity, convexity and combinations of theories, Deciding the word problem in the union of equational theories., Better answers to real questions, A structural/temporal query language for business processes, A rewriting approach to satisfiability procedures., Virtual worlds as meeting places for formal systems, Constraint contextual rewriting., A new combination procedure for the word problem that generalizes fusion decidability results in modal logics, Modular proof systems for partial functions with Evans equality, Efficient theory combination via Boolean search, Decision procedures for term algebras with integer constraints, A taxonomy of exact methods for partial Max-SAT, Combining decision procedures by (model-)equality propagation, Automated verification of shape, size and bag properties via user-defined predicates in separation logic, Modular term rewriting systems and the termination, On deciding satisfiability by theorem proving with speculative inferences, Monotonicity inference for higher-order formulas, A decidability result for the model checking of infinite-state systems, Complexity assessments for decidable fragments of Set Theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages, First-order automated reasoning with theories: when deduction modulo theory meets practice, Being careful about theory combination, Resolution proof transformation for compression and interpolation, An extension of lazy abstraction with interpolation for programs with arrays, Partition-based logical reasoning for first-order and propositional theories, Decision procedures for extensions of the theory of arrays, Solving constraint satisfaction problems with SAT modulo theories, Interpolation and amalgamation for arrays with MaxDiff, Combination techniques and decision problems for disunification, Natural language syntax and first-order inference, Many-sorted equivalence of shiny and strongly polite theories, An efficient SMT solver for string constraints, Producing and verifying extremely large propositional refutations, Canonization for disjoint unions of theories, A randomized satisfiability procedure for arithmetic and uninterpreted function symbols, Automatic decidability and combinability, Sharpening constraint programming approaches for bit-vector theory, Model-theoretic methods in combined constraint satisfiability, A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions. I: The two-level case, IPL: an integration property language for multi-model cyber-physical systems, Common knowledge does not have the Beth property, Unification in a combination of arbitrary disjoint equational theories, Milestones from the Pure Lisp Theorem Prover to ACL2, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates, A semantic approach to interpolation, Order-Sorted Rewriting and Congruence Closure, Politeness and combination methods for theories with bridging functions, Conflict-driven satisfiability for theory combination: transition system and completeness, $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation, Colors Make Theories Hard, Tractable combinations of theories via sampling, Politeness and stable infiniteness: stronger together, Unification modulo lists with reverse relation with certain word equations, Editors' introduction to the special issue on combining logics, Metalevel Algorithms for Variant Satisfiability, Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis, Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations, Theory decision by decomposition, Combination of convex theories: modularity, deduction completeness, and explanation, Towards an integration science. The influence of Richard Bellman on our research., Polite combination of algebraic datatypes, Combination of uniform interpolants via Beth definability, An interpolating theorem prover, Combined covers and Beth definability, Politeness for the theory of algebraic datatypes, Unions of non-disjoint theories and combinations of satisfiability procedures, Model-based Theory Combination, CC(X): Semantic Combination of Congruence Closure with Solvable Theories, An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types, Applications of Hierarchical Reasoning in the Verification of Complex Systems, Programmed Strategies for Program Verification, A posthumous contribution by Larry Wos: excerpts from an unpublished column, Reasoning about vectors using an SMT theory of sequences, Generalised graded interpolation, Essence of generalized partial computation, On interpolation in automated theorem proving, Combining sets with cardinals, A tool for deciding the satisfiability of continuous-time metric temporal logic, Symbolic computation in Maude: some tapas
