Pages that link to "Item:Q1401930"

The following pages link to A rewriting approach to satisfiability procedures. (Q1401930):

Displaying 34 items.

• Interpolation systems for ground proofs in automated deduction: a survey (Q287275) (← links)
• Adding decision procedures to SMT solvers using axioms with triggers (Q287384) (← links)
• On deciding satisfiability by theorem proving with speculative inferences (Q438533) (← links)
• An instantiation scheme for satisfiability modulo theories (Q438578) (← links)
• Automatic decidability and combinability (Q549666) (← links)
• Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) (Q861691) (← links)
• Theory decision by decomposition (Q1041591) (← links)
• Combination of convex theories: modularity, deduction completeness, and explanation (Q1041593) (← links)
• Solving linear optimization over arithmetic constraint formula (Q1675635) (← links)
• Superposition decides the first-order logic fragment over ground theories (Q1949088) (← links)
• A superposition calculus for abductive reasoning (Q2013317) (← links)
• Politeness and combination methods for theories with bridging functions (Q2303236) (← links)
• SMELS: satisfiability modulo equality with lazy superposition (Q2351265) (← links)
• On interpolation in automated theorem proving (Q2352502) (← links)
• Metalevel algorithms for variant satisfiability (Q2413027) (← links)
• Modular proof systems for partial functions with Evans equality (Q2432764) (← links)
• Towards a unified model of search in theorem-proving: subgoal-reduction strategies (Q2456542) (← links)
• Decision procedures for extensions of the theory of arrays (Q2457800) (← links)
• Metalevel Algorithms for Variant Satisfiability (Q2827841) (← links)
• Rewrite-Based Decision Procedures (Q2864358) (← links)
• Rewrite-Based Satisfiability Procedures for Recursive Data Structures (Q2864524) (← links)
• A Rewriting Approach to the Combination of Data Structures with Bridging Theories (Q2964468) (← links)
• Modular Termination and Combinability for Superposition Modulo Counter Arithmetic (Q3172895) (← links)
• SMELS: Satisfiability Modulo Equality with Lazy Superposition (Q3540073) (← links)
• Satisfiability Procedures for Combination of Theories Sharing Integer Offsets (Q3617773) (← links)
• Data Structures with Arithmetic Constraints: A Non-disjoint Combination (Q3655209) (← links)
• Variant-Based Satisfiability in Initial Algebras (Q4686604) (← links)
• Harald Ganzinger’s Legacy: Contributions to Logics and Programming (Q4916069) (← links)
• Canonical Ground Horn Theories (Q4916071) (← links)
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs (Q4916225) (← links)
• On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving (Q5191095) (← links)
• Combinable Extensions of Abelian Groups (Q5191096) (← links)
• Locality Results for Certain Extensions of Theories with Bridging Functions (Q5191097) (← links)
• Equational Theorem Proving for Clauses over Strings (Q6118747) (← links)