Simplification by Cooperating Decision Procedures
From MaRDI portal
Publication:3899468
DOI10.1145/357073.357079zbMath0452.68013MaRDI 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
68Q25: Analysis of algorithms and problem complexity
68W30: Symbolic computation and algebraic computation
68Q60: Specification and verification (program logics, model checking, etc.)
68Q65: Abstract data types; algebraic specification
Related Items
On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving, Combinable Extensions of Abelian Groups, Efficient Interpolant Generation in Satisfiability Modulo Theories, On Hierarchical Reasoning in Combinations of Theories, 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, Unification in a combination of arbitrary disjoint equational theories, Combination techniques and decision problems for disunification, Essence of generalized partial computation, Combining sets with cardinals, Combining nonstably infinite theories, Deciding Boolean algebra with Presburger arithmetic, An institution-independent proof of the Robinson consistency theorem, Modular term rewriting systems and the termination, Common knowledge does not have the Beth property, A semantic approach to interpolation, 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, A decision procedure for combinations of propositional temporal logic and other specialized theories, A structure-preserving clause form translation, Unification in combinations of collapse-free regular theories, Combination of constraint solvers for free and quasi-free structures, Complexity, convexity and combinations of theories, Natural language syntax and first-order inference, An overview of the Tecton proof system, Embedding complex decision procedures inside an interactive theorem prover., Deciding the word problem in the union of equational theories., A rewriting approach to satisfiability procedures., Virtual worlds as meeting places for formal systems, Constraint contextual rewriting., Towards an integration science. The influence of Richard Bellman on our research., Editors' introduction to the special issue on combining logics, Unions of non-disjoint theories and combinations of satisfiability procedures, Structured proof procedures, Strategies for combining decision procedures, 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, Partition-based logical reasoning for first-order and propositional theories, Decision procedures for extensions of the theory of arrays, Canonization for disjoint unions of theories, A randomized satisfiability procedure for arithmetic and uninterpreted function symbols, An interpolating theorem prover, Decision Procedures for Automating Termination Proofs, On the cooperation of the constraint domains ℋ, ℛ, and ℱ in CFLP, Verifying Heap-Manipulating Programs in an SMT Framework, Ground Interpolation for the Theory of Equality, Satisfiability Procedures for Combination of Theories Sharing Integer Offsets, Efficient Term-ITE Conversion for Satisfiability Modulo Theories, 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
