Mnacho Echenim

ORCID

Publication Activity (10 Years)

Years Active: 2003-2024
Publications (10 Years): 40

Top Venues

Grenoble Institute of Technology, France (PHD)

Education History

Grenoble Institute of Technology, France

PHD

Publications

Mnacho Echenim, Mehdi Mhalla
A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL. J. Autom. Reason. 68 (1) (2024)
Mnacho Echenim, Mehdi Mhalla
A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL. CoRR (2023)
Mnacho Echenim, Nicolas Peltier
A Proof Procedure for Separation Logic with Inductive Definitions and Data. J. Autom. Reason. 67 (3) (2023)
Mnacho Echenim, Mehdi Mhalla, Coraline Mori
The CHSH inequality: Tsirelson's upper-bound and other results. Arch. Formal Proofs 2023 (2023)
Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier
A Strict Constrained Superposition Calculus for Graphs. FoSSaCS (2023)
Mnacho Echenim, Nicolas Peltier
An undecidability result for Separation Logic with theory reasoning. Inf. Process. Lett. 182 (2023)
Mnacho Echenim, Nicolas Peltier
Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates. CoRR (2023)
Mnacho Echenim, Nicolas Peltier
A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning. CoRR (2022)
Mnacho Echenim
Simultaneous diagonalization of pairwise commuting Hermitian matrices. Arch. Formal Proofs 2022 (2022)
Mnacho Echenim, Nicolas Peltier
Two Results on Separation Logic With Theory Reasoning. CoRR (2022)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules. Inf. Process. Lett. 173 (2022)
Mnacho Echenim, Mehdi Mhalla
Quantum projective measurements and the CHSH inequality in Isabelle/HOL. CoRR (2021)
Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier
A Superposition-Based Calculus for Diagrammatic Reasoning. PPDP (2021)
Marie Cousin, Mnacho Echenim, Hervé Guiol
The Hahn and Jordan Decomposition Theorems. Arch. Formal Proofs 2021 (2021)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment. CSL (2021)
Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier
A Superposition-Based Calculus for Quantum Diagrammatic Reasoning and Beyond. CoRR (2021)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Unifying Decidable Entailments in Separation Logic with Inductive Definitions. CADE (2021)
Mnacho Echenim
Quantum projective measurements and the CHSH inequality. Arch. Formal Proofs 2021 (2021)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. CoRR (2020)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Checking Entailment Between Separation Logic Symbolic Heaps: Beyond Connected and Established Systems. CoRR (2020)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems. CoRR (2020)
Mnacho Echenim, Nicolas Peltier
Combining Induction and Saturation-Based Theorem Proving. J. Autom. Reason. 64 (2) (2020)
Mnacho Echenim, Hervé Guiol, Nicolas Peltier
Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL. J. Autom. Reason. 64 (4) (2020)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. LPAR (2020)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates. ACM Trans. Comput. Log. 21 (3) (2020)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
Prenex Separation Logic with One Selector Field. TABLEAUX (2019)
Mnacho Echenim, Nicolas Peltier, Yanis Sellami
Ilinva: Using Abduction to Generate Loop Invariants. FroCos (2019)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. FoSSaCS (2019)
Mnacho Echenim, Nicolas Peltier, Yanis Sellami
Ilinva: Using Abduction to Generate Loop Invariants. CoRR (2019)
Mnacho Echenim, Hervé Guiol, Nicolas Peltier
Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL. CoRR (2018)
Mnacho Echenim, Nicolas Peltier, Yanis Sellami
A Generic Framework for Implicate Generation Modulo Theories. CoRR (2018)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic. CoRR (2018)
Mnacho Echenim, Radu Iosif, Nicolas Peltier
The Complexity of Prenex Separation Logic with One Selector. CoRR (2018)
Mnacho Echenim, Nicolas Peltier, Yanis Sellami
A Generic Framework for Implicate Generation Modulo Theories. IJCAR (2018)
Mnacho Echenim
Pricing in discrete financial models. Arch. Formal Proofs 2018 (2018)
Mnacho Echenim, Nicolas Peltier, Sophie Tourret
Prime Implicate Generation in Equational Logic (extended abstract). IJCAI (2018)
Mnacho Echenim, Nicolas Peltier, Sophie Tourret
Prime Implicate Generation in Equational Logic. J. Artif. Intell. Res. 60 (2017)
Mnacho Echenim, Nicolas Peltier
The Binomial Pricing Model in Finance: A Formalization in Isabelle. CADE (2017)
Mnacho Echenim, Nicolas Peltier
A Superposition Calculus for Abductive Reasoning. J. Autom. Reason. 57 (2) (2016)
Mnacho Echenim, Nicolas Peltier, Sophie Tourret
Quantifier-Free Equational Logic and Prime Implicate Generation. CADE (2015)
Mnacho Echenim, Nicolas Peltier, Sophie Tourret
A Rewriting Strategy to Generate Prime Implicates in Equational Logic. IJCAR (2014)
Mnacho Echenim, Nicolas Peltier
A Superposition Calculus for Abductive Reasoning. CoRR (2014)
Sophie Tourret, Mnacho Echenim, Nicolas Peltier
A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses. PAAR@IJCAR (2014)
Mnacho Echenim, Nicolas Peltier, Sophie Tourret
An Approach to Abductive Reasoning in Equational Logic. IJCAI (2013)
Mnacho Echenim, Nicolas Peltier
Instantiation Schemes for Nested Theories. ACM Trans. Comput. Log. 14 (2) (2013)
Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier
A Resolution Calculus for First-order Schemata. Fundam. Informaticae 125 (2) (2013)
Mnacho Echenim, Nicolas Peltier
Reasoning on Schemata of Formulae CoRR (2012)
Mnacho Echenim, Nicolas Peltier
A Calculus for Generating Ground Explanations (Technical Report) CoRR (2012)
Mnacho Echenim, Nicolas Peltier
A Calculus for Generating Ground Explanations. IJCAR (2012)
Mnacho Echenim, Nicolas Peltier
Reasoning on Schemata of Formulæ. AISC/MKM/Calculemus (2012)
Mnacho Echenim, Nicolas Peltier
An Instantiation Scheme for Satisfiability Modulo Theories. J. Autom. Reason. 48 (3) (2012)
Mnacho Echenim, Nicolas Peltier
Modular instantiation schemes. Inf. Process. Lett. 111 (20) (2011)
Mnacho Echenim, Nicolas Peltier
Instantiation Schemes for Nested Theories CoRR (2011)
Thierry Boy de la Tour, Mnacho Echenim
Solving Linear Constraints in Elementary Abelian p-Groups of Symmetries CoRR (2011)
Mnacho Echenim, Nicolas Peltier
Instantiation of SMT Problems Modulo Integers. AISC/MKM/Calculemus (2010)
Mnacho Echenim, Nicolas Peltier
Instantiation of SMT problems modulo Integers CoRR (2010)
Maria Paola Bonacina, Mnacho Echenim
Theory decision by decomposition. J. Symb. Comput. 45 (2) (2010)
Thierry Boy de la Tour, Mnacho Echenim, Paliath Narendran
Unification and Matching Modulo Leaf-Permutative Equational Presentations. IJCAR (2008)
Maria Paola Bonacina, Mnacho Echenim
On Variable-inactivity and Polynomial tau-Satisfiability Procedures. J. Log. Comput. 18 (1) (2008)
Maria Paola Bonacina, Mnacho Echenim
T-Decision by Decomposition. CADE (2007)
Maria Paola Bonacina, Mnacho Echenim
Rewrite-Based Decision Procedures. Electron. Notes Theor. Comput. Sci. 174 (11) (2007)
Maria Paola Bonacina, Mnacho Echenim
Rewrite-Based Satisfiability Procedures for Recursive Data Structures. Electron. Notes Theor. Comput. Sci. 174 (8) (2007)
Thierry Boy de la Tour, Mnacho Echenim
Permutative rewriting and unification. Inf. Comput. 205 (4) (2007)
Thierry Boy de la Tour, Mnacho Echenim
Determining Unify-Stable Presentations. RTA (2007)
Thierry Boy de la Tour, Mnacho Echenim
Unification in a Class of Permutative Theories. RTA (2005)
Thierry Boy de la Tour, Mnacho Echenim
Overlapping Leaf Permutative Equations. IJCAR (2004)
Thierry Boy de la Tour, Mnacho Echenim
On the Complexity of Deduction Modulo Leaf Permutative Equations. J. Autom. Reason. 33 (3-4) (2004)
Thierry Boy de la Tour, Mnacho Echenim
NP-Completeness Results for Deductive Problems on Stratified Terms. LPAR (2003)
Thierry Boy de la Tour, Mnacho Echenim
On Leaf Permutative Theories and Occurrence Permutation Groups. Electron. Notes Theor. Comput. Sci. 86 (1) (2003)

Mnacho Echenim.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Mnacho Echenim