default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDMnacho Echenim
Person information
- affiliation: Grenoble Alpes University, CNRS, France
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[j22]Mnacho Echenim, Mehdi Mhalla:
A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL. J. Autom. Reason. 68(1): 2 (2024)- 2023
- [j21]Mnacho Echenim, Mehdi Mhalla, Coraline Mori:
The CHSH inequality: Tsirelson's upper-bound and other results. Arch. Formal Proofs 2023 (2023) - [j20]Mnacho Echenim, Nicolas Peltier
:
An undecidability result for Separation Logic with theory reasoning. Inf. Process. Lett. 182: 106359 (2023) - [j19]Mnacho Echenim, Nicolas Peltier:
A Proof Procedure for Separation Logic with Inductive Definitions and Data. J. Autom. Reason. 67(3): 30 (2023) - [c27]Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier:
A Strict Constrained Superposition Calculus for Graphs. FoSSaCS 2023: 135-155 - [i20]Mnacho Echenim, Nicolas Peltier:
Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates. CoRR abs/2305.08419 (2023) - [i19]Mnacho Echenim, Mehdi Mhalla:
A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL. CoRR abs/2306.12535 (2023) - 2022
- [j18]Mnacho Echenim:
Simultaneous diagonalization of pairwise commuting Hermitian matrices. Arch. Formal Proofs 2022 (2022) - [j17]Mnacho Echenim, Radu Iosif, Nicolas Peltier:
Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules. Inf. Process. Lett. 173: 106169 (2022) - [i18]Mnacho Echenim, Nicolas Peltier:
A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning. CoRR abs/2201.13227 (2022) - [i17]Mnacho Echenim, Nicolas Peltier:
Two Results on Separation Logic With Theory Reasoning. CoRR abs/2206.09389 (2022) - 2021
- [j16]Marie Cousin, Mnacho Echenim, Hervé Guiol:
The Hahn and Jordan Decomposition Theorems. Arch. Formal Proofs 2021 (2021) - [j15]Mnacho Echenim:
Quantum projective measurements and the CHSH inequality. Arch. Formal Proofs 2021 (2021) - [c26]Mnacho Echenim, Radu Iosif, Nicolas Peltier:
Unifying Decidable Entailments in Separation Logic with Inductive Definitions. CADE 2021: 183-199 - [c25]Mnacho Echenim, Radu Iosif, Nicolas Peltier:
Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment. CSL 2021: 20:1-20:18 - [c24]Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier:
A Superposition-Based Calculus for Diagrammatic Reasoning. PPDP 2021: 10:1-10:13 - [i16]Mnacho Echenim, Mehdi Mhalla:
Quantum projective measurements and the CHSH inequality in Isabelle/HOL. CoRR abs/2103.08535 (2021) - [i15]Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier:
A Superposition-Based Calculus for Quantum Diagrammatic Reasoning and Beyond. CoRR abs/2103.11709 (2021) - 2020
- [j14]Mnacho Echenim, Nicolas Peltier:
Combining Induction and Saturation-Based Theorem Proving. J. Autom. Reason. 64(2): 253-294 (2020) - [j13]Mnacho Echenim, Hervé Guiol, Nicolas Peltier:
Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL. J. Autom. Reason. 64(4): 737-765 (2020) - [j12]Mnacho Echenim, Radu Iosif, Nicolas Peltier:
The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates. ACM Trans. Comput. Log. 21(3): 19:1-19:46 (2020) - [c23]Mnacho Echenim, Radu Iosif, Nicolas Peltier:
Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. LPAR 2020: 191-211 - [i14]Mnacho Echenim, Radu Iosif, Nicolas Peltier:
Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. CoRR abs/2004.07578 (2020) - [i13]Mnacho Echenim, Radu Iosif, Nicolas Peltier:
Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems. CoRR abs/2007.00502 (2020) - [i12]Mnacho Echenim, Radu Iosif, Nicolas Peltier:
Checking Entailment Between Separation Logic Symbolic Heaps: Beyond Connected and Established Systems. CoRR abs/2012.14361 (2020)
2010 – 2019
- 2019
- [c22]Mnacho Echenim, Radu Iosif, Nicolas Peltier:
The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. FoSSaCS 2019: 242-259 - [c21]Mnacho Echenim, Nicolas Peltier, Yanis Sellami:
Ilinva: Using Abduction to Generate Loop Invariants. FroCos 2019: 77-93 - [c20]Mnacho Echenim, Radu Iosif, Nicolas Peltier:
Prenex Separation Logic with One Selector Field. TABLEAUX 2019: 409-427 - [i11]Mnacho Echenim, Nicolas Peltier, Yanis Sellami:
Ilinva: Using Abduction to Generate Loop Invariants. CoRR abs/1906.11033 (2019) - 2018
- [j11]Mnacho Echenim:
Pricing in discrete financial models. Arch. Formal Proofs 2018 (2018) - [c19]Mnacho Echenim, Nicolas Peltier, Yanis Sellami:
A Generic Framework for Implicate Generation Modulo Theories. IJCAR 2018: 279-294 - [c18]Mnacho Echenim, Nicolas Peltier, Sophie Tourret:
Prime Implicate Generation in Equational Logic (extended abstract). IJCAI 2018: 5588-5592 - [i10]Mnacho Echenim, Radu Iosif, Nicolas Peltier:
On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic. CoRR abs/1802.00195 (2018) - [i9]Mnacho Echenim, Radu Iosif, Nicolas Peltier:
The Complexity of Prenex Separation Logic with One Selector. CoRR abs/1804.03556 (2018) - [i8]Mnacho Echenim, Nicolas Peltier, Yanis Sellami:
A Generic Framework for Implicate Generation Modulo Theories. CoRR abs/1807.04557 (2018) - [i7]Mnacho Echenim, Hervé Guiol, Nicolas Peltier:
Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL. CoRR abs/1807.09873 (2018) - 2017
- [j10]Mnacho Echenim, Nicolas Peltier, Sophie Tourret:
Prime Implicate Generation in Equational Logic. J. Artif. Intell. Res. 60: 827-880 (2017) - [c17]Mnacho Echenim, Nicolas Peltier:
The Binomial Pricing Model in Finance: A Formalization in Isabelle. CADE 2017: 546-562 - 2016
- [j9]Mnacho Echenim, Nicolas Peltier:
A Superposition Calculus for Abductive Reasoning. J. Autom. Reason. 57(2): 97-134 (2016) - 2015
- [c16]Mnacho Echenim, Nicolas Peltier, Sophie Tourret:
Quantifier-Free Equational Logic and Prime Implicate Generation. CADE 2015: 311-325 - 2014
- [c15]Sophie Tourret, Mnacho Echenim, Nicolas Peltier:
A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses. PAAR@IJCAR 2014: 94-104 - [c14]Mnacho Echenim, Nicolas Peltier, Sophie Tourret:
A Rewriting Strategy to Generate Prime Implicates in Equational Logic. IJCAR 2014: 137-151 - [i6]Mnacho Echenim, Nicolas Peltier:
A Superposition Calculus for Abductive Reasoning. CoRR abs/1406.0303 (2014) - 2013
- [j8]Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier:
A Resolution Calculus for First-order Schemata. Fundam. Informaticae 125(2): 101-133 (2013) - [j7]Mnacho Echenim, Nicolas Peltier:
Instantiation Schemes for Nested Theories. ACM Trans. Comput. Log. 14(2): 11:1-11:34 (2013) - [c13]Mnacho Echenim, Nicolas Peltier, Sophie Tourret:
An Approach to Abductive Reasoning in Equational Logic. IJCAI 2013: 531-537 - 2012
- [j6]Mnacho Echenim, Nicolas Peltier:
An Instantiation Scheme for Satisfiability Modulo Theories. J. Autom. Reason. 48(3): 293-362 (2012) - [c12]Mnacho Echenim, Nicolas Peltier:
Reasoning on Schemata of Formulæ. AISC/MKM/Calculemus 2012: 310-325 - [c11]Mnacho Echenim, Nicolas Peltier:
A Calculus for Generating Ground Explanations. IJCAR 2012: 194-209 - [i5]Mnacho Echenim, Nicolas Peltier:
A Calculus for Generating Ground Explanations (Technical Report). CoRR abs/1201.5954 (2012) - [i4]Mnacho Echenim, Nicolas Peltier:
Reasoning on Schemata of Formulae. CoRR abs/1204.2990 (2012) - 2011
- [j5]Mnacho Echenim, Nicolas Peltier:
Modular instantiation schemes. Inf. Process. Lett. 111(20): 989-993 (2011) - [i3]Thierry Boy de la Tour, Mnacho Echenim:
Solving Linear Constraints in Elementary Abelian p-Groups of Symmetries. CoRR abs/1107.4553 (2011) - [i2]Mnacho Echenim, Nicolas Peltier:
Instantiation Schemes for Nested Theories. CoRR abs/1107.4937 (2011) - 2010
- [j4]Maria Paola Bonacina, Mnacho Echenim:
Theory decision by decomposition. J. Symb. Comput. 45(2): 229-260 (2010) - [c10]Mnacho Echenim, Nicolas Peltier:
Instantiation of SMT Problems Modulo Integers. AISC/MKM/Calculemus 2010: 49-63 - [i1]Mnacho Echenim, Nicolas Peltier:
Instantiation of SMT problems modulo Integers. CoRR abs/1006.2921 (2010)
2000 – 2009
- 2008
- [j3]Maria Paola Bonacina, Mnacho Echenim:
On Variable-inactivity and Polynomial tau-Satisfiability Procedures. J. Log. Comput. 18(1): 77-96 (2008) - [c9]Thierry Boy de la Tour, Mnacho Echenim, Paliath Narendran:
Unification and Matching Modulo Leaf-Permutative Equational Presentations. IJCAR 2008: 332-347 - 2007
- [j2]Thierry Boy de la Tour, Mnacho Echenim:
Permutative rewriting and unification. Inf. Comput. 205(4): 624-650 (2007) - [c8]Maria Paola Bonacina, Mnacho Echenim:
T-Decision by Decomposition. CADE 2007: 199-214 - [c7]Thierry Boy de la Tour, Mnacho Echenim:
Determining Unify-Stable Presentations. RTA 2007: 63-77 - 2006
- [c6]Maria Paola Bonacina, Mnacho Echenim:
Rewrite-Based Decision Procedures. STRATEGIES@IJCAR 2006: 27-45 - [c5]Maria Paola Bonacina, Mnacho Echenim:
Rewrite-Based Satisfiability Procedures for Recursive Data Structures. PDPAR/PaUL@FLoC 2006: 55-70 - 2005
- [b1]Mnacho Echenim:
Déduction et Unification dans les Théories Permutatives. (Deduction and Unification in Permutative Theories). Grenoble Institute of Technology, France, 2005 - [c4]Thierry Boy de la Tour, Mnacho Echenim:
Unification in a Class of Permutative Theories. RTA 2005: 105-119 - 2004
- [j1]Thierry Boy de la Tour, Mnacho Echenim:
On the Complexity of Deduction Modulo Leaf Permutative Equations. J. Autom. Reason. 33(3-4): 271-317 (2004) - [c3]Thierry Boy de la Tour, Mnacho Echenim:
Overlapping Leaf Permutative Equations. IJCAR 2004: 430-444 - 2003
- [c2]Thierry Boy de la Tour, Mnacho Echenim:
NP-Completeness Results for Deductive Problems on Stratified Terms. LPAR 2003: 317-331 - [c1]Thierry Boy de la Tour, Mnacho Echenim:
On Leaf Permutative Theories and Occurrence Permutation Groups. FTP 2003: 61-75
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-01-21 00:15 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
