Pages that link to "Item:Q5277822"
From MaRDI portal
The following pages link to New results on rewrite-based satisfiability procedures (Q5277822):
Displayed 31 items.
- Interpolation systems for ground proofs in automated deduction: a survey (Q287275) (← links)
- Theory decision by decomposition (Q1041591) (← links)
- Combination of convex theories: modularity, deduction completeness, and explanation (Q1041593) (← links)
- Superposition as a decision procedure for timed automata (Q1949086) (← links)
- Superposition decides the first-order logic fragment over ground theories (Q1949088) (← links)
- A superposition calculus for abductive reasoning (Q2013317) (← links)
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates (Q2031420) (← links)
- Polite combination of algebraic datatypes (Q2090130) (← links)
- Politeness for the theory of algebraic datatypes (Q2096449) (← links)
- Larry Wos: visions of automated reasoning (Q2102922) (← links)
- Set of support, demodulation, paramodulation: a historical perspective (Q2102923) (← links)
- Politeness and combination methods for theories with bridging functions (Q2303236) (← links)
- Unification modulo lists with reverse relation with certain word equations (Q2305403) (← links)
- On interpolation in automated theorem proving (Q2352502) (← links)
- Weakly Equivalent Arrays (Q2964457) (← 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)
- Quantifier-Free Equational Logic and Prime Implicate Generation (Q3454103) (← links)
- A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited (Q3454111) (← links)
- Engineering DPLL(T) + Saturation (Q3541724) (← links)
- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets (Q3617773) (← links)
- Superposition Modulo Linear Arithmetic SUP(LA) (Q3655193) (← links)
- Data Structures with Arithmetic Constraints: A Non-disjoint Combination (Q3655209) (← links)
- Variant-Based Satisfiability in Initial Algebras (Q4686604) (← links)
- Superposition for Bounded Domains (Q4913861) (← links)
- Harald Ganzinger’s Legacy: Contributions to Logics and Programming (Q4916069) (← links)
- Canonical Ground Horn Theories (Q4916071) (← links)
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving (Q5191095) (← links)
- Combinable Extensions of Abelian Groups (Q5191096) (← links)
- Heaps and Data Structures: A Challenge for Automated Provers (Q5200023) (← links)
- Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties (Q6135743) (← links)