Pages that link to "Item:Q3899468"

The following pages link to Simplification by Cooperating Decision Procedures (Q3899468):

Displaying 50 items.

• A tool for deciding the satisfiability of continuous-time metric temporal logic (Q262137) (← links)
• Proof tree preserving tree interpolation (Q286737) (← links)
• Interpolation systems for ground proofs in automated deduction: a survey (Q287275) (← links)
• A heuristic prover for real inequalities (Q287379) (← links)
• Rewriting modulo SMT and open system analysis (Q347384) (← links)
• A structural/temporal query language for business processes (Q414923) (← links)
• Combining decision procedures by (model-)equality propagation (Q436376) (← links)
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic (Q436400) (← links)
• On deciding satisfiability by theorem proving with speculative inferences (Q438533) (← links)
• Monotonicity inference for higher-order formulas (Q438558) (← links)
• A decidability result for the model checking of infinite-state systems (Q438572) (← links)
• Resolution proof transformation for compression and interpolation (Q479815) (← links)
• An extension of lazy abstraction with interpolation for programs with arrays (Q479820) (← links)
• Solving constraint satisfaction problems with SAT modulo theories (Q487632) (← links)
• An efficient SMT solver for string constraints (Q518402) (← links)
• Automatic decidability and combinability (Q549666) (← links)
• Model-theoretic methods in combined constraint satisfiability (Q556677) (← links)
• A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions. I: The two-level case (Q556680) (← links)
• Unification in a combination of arbitrary disjoint equational theories (Q582270) (← links)
• Combination techniques and decision problems for disunification (Q673624) (← links)
• Many-sorted equivalence of shiny and strongly polite theories (Q682380) (← links)
• Producing and verifying extremely large propositional refutations (Q694550) (← links)
• Essence of generalized partial computation (Q808278) (← links)
• Combining sets with cardinals (Q812443) (← links)
• Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (Q832719) (← links)
• Combining nonstably infinite theories (Q851136) (← links)
• Deciding Boolean algebra with Presburger arithmetic (Q861705) (← links)
• An institution-independent proof of the Robinson consistency theorem (Q878156) (← links)
• An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty (Q892228) (← links)
• Better answers to real questions (Q898260) (← links)
• Modular term rewriting systems and the termination (Q910207) (← links)
• Common knowledge does not have the Beth property (Q987837) (← links)
• A semantic approach to interpolation (Q1006639) (← links)
• Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis (Q1037399) (← links)
• Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations (Q1039847) (← links)
• Theory decision by decomposition (Q1041591) (← links)
• Combination of convex theories: modularity, deduction completeness, and explanation (Q1041593) (← links)
• A decision procedure for combinations of propositional temporal logic and other specialized theories (Q1097264) (← links)
• A structure-preserving clause form translation (Q1098330) (← links)
• Unification in combinations of collapse-free regular theories (Q1099652) (← links)
• Combination of constraint solvers for free and quasi-free structures (Q1127338) (← links)
• Complexity, convexity and combinations of theories (Q1141138) (← links)
• Natural language syntax and first-order inference (Q1193491) (← links)
• An overview of the Tecton proof system (Q1341710) (← links)
• Embedding complex decision procedures inside an interactive theorem prover. (Q1353946) (← links)
• Deciding the word problem in the union of equational theories. (Q1400706) (← links)
• A rewriting approach to satisfiability procedures. (Q1401930) (← links)
• Virtual worlds as meeting places for formal systems (Q1402195) (← links)
• Constraint contextual rewriting. (Q1404984) (← links)
• Towards an integration science. The influence of Richard Bellman on our research. (Q1584626) (← links)