The following pages link to Mnacho Echenim (Q438577):
Displaying 37 items.
- An instantiation scheme for satisfiability modulo theories (Q438578) (← links)
- On the complexity of deduction modulo leaf permutative equations (Q556681) (← links)
- Permutative rewriting and unification (Q876048) (← links)
- Theory decision by decomposition (Q1041591) (← links)
- A generic framework for implicate generation modulo theories (Q1799090) (← links)
- Modular instantiation schemes (Q1944184) (← links)
- Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL (Q1984795) (← links)
- A superposition calculus for abductive reasoning (Q2013317) (← links)
- Unifying decidable entailments in separation logic with inductive definitions (Q2055854) (← links)
- Ilinva: using abduction to generate loop invariants (Q2180218) (← links)
- Prenex separation logic with one selector field (Q2180532) (← links)
- Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules (Q2234797) (← links)
- The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains (Q2289076) (← links)
- Combining induction and saturation-based theorem proving (Q2303240) (← links)
- The binomial pricing model in finance: a formalization in Isabelle (Q2405273) (← links)
- A Resolution Calculus for First-order Schemata (Q2843818) (← links)
- Rewrite-Based Decision Procedures (Q2864358) (← links)
- Rewrite-Based Satisfiability Procedures for Recursive Data Structures (Q2864524) (← links)
- Reasoning on Schemata of Formulæ (Q2907331) (← links)
- A Calculus for Generating Ground Explanations (Q2908490) (← links)
- Instantiation Schemes for Nested Theories (Q2946696) (← links)
- A Rewriting Strategy to Generate Prime Implicates in Equational Logic (Q3192186) (← links)
- (Q3408147) (← links)
- Quantifier-Free Equational Logic and Prime Implicate Generation (Q3454103) (← links)
- Unification and Matching Modulo Leaf-Permutative Equational Presentations (Q3541715) (← links)
- Instantiation of SMT Problems Modulo Integers (Q3582696) (← links)
- ${\mathcal{T}}$ -Decision by Decomposition (Q3608774) (← links)
- Prime Implicate Generation in Equational Logic (Q4600725) (← links)
- On leaf permutative theories and occurrence permutation groups (Q4916222) (← links)
- The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates (Q5121270) (← links)
- Automated Reasoning (Q5307078) (← links)
- Determining Unify-Stable Presentations (Q5432333) (← links)
- On Variable-inactivity and Polynomial Formula-Satisfiability Procedures (Q5450569) (← links)
- Term Rewriting and Applications (Q5703878) (← links)
- A proof procedure for separation logic with inductive definitions and data (Q6053843) (← links)
- An undecidability result for separation logic with theory reasoning (Q6161426) (← links)
- A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL (Q6190081) (← links)
