NP-Completeness Results for Deductive Problems on Stratified Terms. - Thierry Boy de la Tour; Mnacho Echenim (LPAR, 2003)

On Leaf Permutative Theories and Occurrence Permutation Groups. - Thierry Boy de la Tour; Mnacho Echenim (FTP, 2003)

Overlapping Leaf Permutative Equations. - Thierry Boy de la Tour; Mnacho Echenim (IJCAR, 2004)

On the Complexity of Deduction Modulo Leaf Permutative Equations. - Thierry Boy de la Tour; Mnacho Echenim (J. Autom. Reason., 2004)

Unification in a Class of Permutative Theories. - Thierry Boy de la Tour; Mnacho Echenim (RTA, 2005)

Déduction et Unification dans les Théories Permutatives. (Deduction and Unification in Permutative Theories). - Mnacho Echenim (2005)

Rewrite-Based Satisfiability Procedures for Recursive Data Structures. - Maria Paola Bonacina; Mnacho Echenim (PDPAR/PaUL@FLoC, 2006)

Rewrite-Based Decision Procedures. - Maria Paola Bonacina; Mnacho Echenim (STRATEGIES@IJCAR, 2006)

T-Decision by Decomposition. - Maria Paola Bonacina; Mnacho Echenim (CADE, 2007)

Determining Unify-Stable Presentations. - Thierry Boy de la Tour; Mnacho Echenim (RTA, 2007)

Permutative rewriting and unification. - Thierry Boy de la Tour; Mnacho Echenim (Inf. Comput., 2007)

Unification and Matching Modulo Leaf-Permutative Equational Presentations. - Thierry Boy de la Tour; Mnacho Echenim; Paliath Narendran (IJCAR, 2008)

On Variable-inactivity and Polynomial tau-Satisfiability Procedures. - Maria Paola Bonacina; Mnacho Echenim (J. Log. Comput., 2008)

Instantiation of SMT Problems Modulo Integers. - Mnacho Echenim; Nicolas Peltier (AISC/MKM/Calculemus, 2010)

Theory decision by decomposition. - Maria Paola Bonacina; Mnacho Echenim (J. Symb. Comput., 2010)

Solving Linear Constraints in Elementary Abelian p-Groups of Symmetries - Thierry Boy de la Tour; Mnacho Echenim (CoRR, 2011)

Modular instantiation schemes. - Mnacho Echenim; Nicolas Peltier (Inf. Process. Lett., 2011)

Reasoning on Schemata of Formulæ. - Mnacho Echenim; Nicolas Peltier (AISC/MKM/Calculemus, 2012)

A Calculus for Generating Ground Explanations. - Mnacho Echenim; Nicolas Peltier (IJCAR, 2012)

A Calculus for Generating Ground Explanations (Technical Report) - Mnacho Echenim; Nicolas Peltier (CoRR, 2012)

An Instantiation Scheme for Satisfiability Modulo Theories. - Mnacho Echenim; Nicolas Peltier (J. Autom. Reason., 2012)

An Approach to Abductive Reasoning in Equational Logic. - Mnacho Echenim; Nicolas Peltier; Sophie Tourret (IJCAI, 2013)

A Resolution Calculus for First-order Schemata. - Vincent Aravantinos; Mnacho Echenim; Nicolas Peltier (Fundam. Informaticae, 2013)

Instantiation Schemes for Nested Theories. - Mnacho Echenim; Nicolas Peltier (ACM Trans. Comput. Log., 2013)

A Rewriting Strategy to Generate Prime Implicates in Equational Logic. - Mnacho Echenim; Nicolas Peltier; Sophie Tourret (IJCAR, 2014)

A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses. - Sophie Tourret; Mnacho Echenim; Nicolas Peltier (PAAR@IJCAR, 2014)

Quantifier-Free Equational Logic and Prime Implicate Generation. - Mnacho Echenim; Nicolas Peltier; Sophie Tourret (CADE, 2015)

A Superposition Calculus for Abductive Reasoning. - Mnacho Echenim; Nicolas Peltier (J. Autom. Reason., 2016)

The Binomial Pricing Model in Finance: A Formalization in Isabelle. - Mnacho Echenim; Nicolas Peltier (CADE, 2017)

Prime Implicate Generation in Equational Logic. - Mnacho Echenim; Nicolas Peltier; Sophie Tourret (J. Artif. Intell. Res., 2017)

A Generic Framework for Implicate Generation Modulo Theories. - Mnacho Echenim; Nicolas Peltier; Yanis Sellami (IJCAR, 2018)

Prime Implicate Generation in Equational Logic (extended abstract). - Mnacho Echenim; Nicolas Peltier; Sophie Tourret (IJCAI, 2018)

Pricing in discrete financial models. - Mnacho Echenim (Arch. Formal Proofs, 2018)

On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (CoRR, 2018)

The Complexity of Prenex Separation Logic with One Selector. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (CoRR, 2018)

The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (FoSSaCS, 2019)

Ilinva: Using Abduction to Generate Loop Invariants. - Mnacho Echenim; Nicolas Peltier; Yanis Sellami (FroCos, 2019)

Prenex Separation Logic with One Selector Field. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (TABLEAUX, 2019)

Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (LPAR, 2020)

Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (CoRR, 2020)

Checking Entailment Between Separation Logic Symbolic Heaps: Beyond Connected and Established Systems. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (CoRR, 2020)

Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL. - Mnacho Echenim; Hervé Guiol; Nicolas Peltier (J. Autom. Reason., 2020)

Combining Induction and Saturation-Based Theorem Proving. - Mnacho Echenim; Nicolas Peltier (J. Autom. Reason., 2020)

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (ACM Trans. Comput. Log., 2020)

Unifying Decidable Entailments in Separation Logic with Inductive Definitions. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (CADE, 2021)

Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (CSL, 2021)

A Superposition-Based Calculus for Diagrammatic Reasoning. - Rachid Echahed; Mnacho Echenim; Mehdi Mhalla; Nicolas Peltier (PPDP, 2021)

The Hahn and Jordan Decomposition Theorems. - Marie Cousin; Mnacho Echenim; Hervé Guiol (Arch. Formal Proofs, 2021)

Quantum projective measurements and the CHSH inequality. - Mnacho Echenim (Arch. Formal Proofs, 2021)

Quantum projective measurements and the CHSH inequality in Isabelle/HOL. - Mnacho Echenim; Mehdi Mhalla (CoRR, 2021)

A Superposition-Based Calculus for Quantum Diagrammatic Reasoning and Beyond. - Rachid Echahed; Mnacho Echenim; Mehdi Mhalla; Nicolas Peltier (CoRR, 2021)

Simultaneous diagonalization of pairwise commuting Hermitian matrices. - Mnacho Echenim (Arch. Formal Proofs, 2022)

A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning. - Mnacho Echenim; Nicolas Peltier (CoRR, 2022)

Two Results on Separation Logic With Theory Reasoning. - Mnacho Echenim; Nicolas Peltier (CoRR, 2022)

Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules. - Mnacho Echenim; Radu Iosif; Nicolas Peltier (Inf. Process. Lett., 2022)

A Strict Constrained Superposition Calculus for Graphs. - Rachid Echahed; Mnacho Echenim; Mehdi Mhalla; Nicolas Peltier (FoSSaCS, 2023)

The CHSH inequality: Tsirelson's upper-bound and other results. - Mnacho Echenim; Mehdi Mhalla; Coraline Mori (Arch. Formal Proofs, 2023)

Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates. - Mnacho Echenim; Nicolas Peltier (CoRR, 2023)

An undecidability result for Separation Logic with theory reasoning. - Mnacho Echenim; Nicolas Peltier (Inf. Process. Lett., 2023)

A Proof Procedure for Separation Logic with Inductive Definitions and Data. - Mnacho Echenim; Nicolas Peltier (J. Autom. Reason., 2023)

A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL. - Mnacho Echenim; Mehdi Mhalla (J. Autom. Reason., 2024)

A Direct Procedure to Test Entailment in a Separation Logic of Relations. - Mnacho Echenim; Nicolas Peltier (J. Autom. Reason., 2025)