I am a professor at Grenoble INP – Ensimag. I obtained my PhD in 2005 under the supervision of Thierry Boy de la Tour and Ricardo Caferra, and received a PhD award from INPG. I did postdoctoral research at the University of Verona (Italy) under the supervision of Maria Paola Bonacina before being recruited at Ensimag. I defended my Habilitation thesis on Nov. 9th, 2017. The manuscript (in french) is available here.
I am mainly interested in automated reasoning, and have currently been working on:
- Separation logic
- The certification of quantum properties
- The formalization of financial mathematics
- Automated theorem provers for solving SMT problems
- Finite instantiation methods
- Inductive reasoning
- Abductive reasoning
I have recently been interested in the formalization of financial mathematics using the proof assistant Isabelle. A zipped folder containing results about the formalization in Isabelle of the Cox-Ross-Rubinstein model can be found here, though it strongly recommended to get the theory files available on the Archive of Formal Proofs.
Publications
Below is an outdated list of publications. A more complete list is available here.
Journal proceedings
- Mnacho Echenim, Nicolas Peltier and Sophie Tourret. Prime Implicate Generation in Equational Logic. Journal of Artificial Intelligence Research, 2017 (DOI). Paper
- Mnacho Echenim and Nicolas Peltier. A Superposition Calculus for Abductive Reasoning. Journal of Automated Reasoning, 2016. Paper
- Vincent Aravantinos, Mnacho Echenim, and Nicolas Peltier. A resolution calculus for first-order schemata. Fundamenta Informaticae, 125(2):101133, 2013. Paper
- Mnacho Echenim and Nicolas Peltier. Instantiation Schemes for Nested Theories. ACM Transactions on Computational Logic, 14(2):11, 2013. Paper
- Mnacho Echenim and Nicolas Peltier. An instantiation scheme for satisfiability modulo theories. Journal of Automated Reasoning, 48(3), 2012. Paper
Conference and workshop proceedings
- M. Echenim, N. Peltier, and S. Tourret. Quantifier-Free Equational Logic and Prime Implicate Generation. CADE 25, 2015. Paper
- M. Echenim, N. Peltier, and S. Tourret. A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses. PAAR 2014. Paper
- M. Echenim, N. Peltier, and S. Tourret. A Rewriting Strategy to Generate Prime Implicates in Equational Logic. IJCAR 2014. Paper
- M. Echenim, N. Peltier, and S. Tourret. An approach to abductive reasoning in equational logic. IJCAI 2013. Extended version
Teaching
I have been co-head of the Financial Engineering department at Ensimag since 2009. These past years, I have been in charge of the following classes:
- Formal Language Theory (Bac + 3). A possibly outdated version of the course notes (in french) is available here.
- Logic bases for Computer Science (Bac + 4). The course notes (in french) are available here. A couple of videos of the lectures (in french) are available below:
- Systematic strategies with .NET (Bac + 5)
Contact Information
Office: LIG, Bâtiment IMAG. 700 avenue Centrale. 38401 St Martin d’Hères. FRANCE
Phone: +33 4 57 42 14 91
Email: Mnacho (dot) Echenim (at) univ-grenoble-alpes (dot) fr
