We stand with Ukraine

We stand with Ukraine

Mnacho Echenim

Orcid: 0000-0001-5765-0758

Affiliations:

Grenoble Alpes University, CNRS, France

According to our database¹, Mnacho Echenim authored at least 61 papers between 2003 and 2024.

Collaborative distances:

Dijkstra number² of four.
Erdős number³ of four.

Timeline

Legend:

Book

In proceedings

Article

PhD thesis

Dataset

Other

Links

Online presence:

on orcid.org

On csauthors.net:

Bibliography

2024

A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL.

[BibT_eX]

[DOI]

,

J. Autom. Reason., March, 2024

2023

A Proof Procedure for Separation Logic with Inductive Definitions and Data.

[BibT_eX]

[DOI]

,

Nicolas Peltier

J. Autom. Reason., September, 2023

An undecidability result for Separation Logic with theory reasoning.

[BibT_eX]

[DOI]

,

Nicolas Peltier

Inf. Process. Lett., August, 2023

Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates.

[BibT_eX]

[DOI]

,

Nicolas Peltier

CoRR, 2023

The CHSH inequality: Tsirelson's upper-bound and other results.

[BibT_eX]

[DOI]

,

,

Arch. Formal Proofs, 2023

A Strict Constrained Superposition Calculus for Graphs.

[BibT_eX]

[DOI]

,

,

,

Nicolas Peltier

Proceedings of the Foundations of Software Science and Computation Structures, 2023

2022

Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules.

[BibT_eX]

[DOI]

,

,

Nicolas Peltier

Inf. Process. Lett., 2022

Two Results on Separation Logic With Theory Reasoning.

[BibT_eX]

[DOI]

,

Nicolas Peltier

CoRR, 2022

A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning.

[BibT_eX]

[DOI]

,

Nicolas Peltier

CoRR, 2022

Simultaneous diagonalization of pairwise commuting Hermitian matrices.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2022

2021

A Superposition-Based Calculus for Quantum Diagrammatic Reasoning and Beyond.

[BibT_eX]

[DOI]

,

,

,

Nicolas Peltier

CoRR, 2021

Quantum projective measurements and the CHSH inequality in Isabelle/HOL.

[BibT_eX]

[DOI]

,

CoRR, 2021

Quantum projective measurements and the CHSH inequality.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

The Hahn and Jordan Decomposition Theorems.

[BibT_eX]

[DOI]

,

,

Arch. Formal Proofs, 2021

A Superposition-Based Calculus for Diagrammatic Reasoning.

[BibT_eX]

[DOI]

,

,

,

Nicolas Peltier

Proceedings of the PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming, 2021

Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment.

[BibT_eX]

[DOI]

,

,

Nicolas Peltier

Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, 2021

Unifying Decidable Entailments in Separation Logic with Inductive Definitions.

[BibT_eX]

[DOI]

,

,

Nicolas Peltier

Proceedings of the Automated Deduction - CADE 28, 2021

2020

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates.

[BibT_eX]

[DOI]

,

,

Nicolas Peltier

ACM Trans. Comput. Log., 2020

Combining Induction and Saturation-Based Theorem Proving.

[BibT_eX]

[DOI]

,

Nicolas Peltier

J. Autom. Reason., 2020

Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL.

[BibT_eX]

[DOI]

,

,

Nicolas Peltier

J. Autom. Reason., 2020

Checking Entailment Between Separation Logic Symbolic Heaps: Beyond Connected and Established Systems.

[BibT_eX]

[DOI]

,

,

Nicolas Peltier

CoRR, 2020

Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems.

[BibT_eX]

[DOI]

,

,

Nicolas Peltier

CoRR, 2020

Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard.

[BibT_eX]

[DOI]

,

,

Nicolas Peltier

Proceedings of the LPAR 2020: 23rd International Conference on Logic for Programming, 2020

2019

Prenex Separation Logic with One Selector Field.

[BibT_eX]

[DOI]

,

,

Nicolas Peltier

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2019

Ilinva: Using Abduction to Generate Loop Invariants.

[BibT_eX]

[DOI]

,

Nicolas Peltier

,

Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains.

[BibT_eX]

[DOI]

,

,

Nicolas Peltier

Proceedings of the Foundations of Software Science and Computation Structures, 2019

2018

The Complexity of Prenex Separation Logic with One Selector.

[BibT_eX]

[DOI]

,

,

Nicolas Peltier

CoRR, 2018

On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic.

[BibT_eX]

[DOI]

,

,

Nicolas Peltier

CoRR, 2018

Pricing in discrete financial models.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

Prime Implicate Generation in Equational Logic (extended abstract).

[BibT_eX]

[DOI]

,

Nicolas Peltier

,

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018

A Generic Framework for Implicate Generation Modulo Theories.

[BibT_eX]

[DOI]

,

Nicolas Peltier

,

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

Prime Implicate Generation in Equational Logic.

[BibT_eX]

[DOI]

,

Nicolas Peltier

,

J. Artif. Intell. Res., 2017

The Binomial Pricing Model in Finance: A Formalization in Isabelle.

[BibT_eX]

[DOI]

,

Nicolas Peltier

Proceedings of the Automated Deduction - CADE 26, 2017

2016

A Superposition Calculus for Abductive Reasoning.

[BibT_eX]

[DOI]

,

Nicolas Peltier

J. Autom. Reason., 2016

2015

Quantifier-Free Equational Logic and Prime Implicate Generation.

[BibT_eX]

[DOI]

,

Nicolas Peltier

,

Proceedings of the Automated Deduction - CADE-25, 2015

2014

A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses.

[BibT_eX]

[DOI]

,

,

Nicolas Peltier

Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

A Rewriting Strategy to Generate Prime Implicates in Equational Logic.

[BibT_eX]

[DOI]

,

Nicolas Peltier

,

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Instantiation Schemes for Nested Theories.

[BibT_eX]

[DOI]

,

Nicolas Peltier

ACM Trans. Comput. Log., 2013

A Resolution Calculus for First-order Schemata.

[BibT_eX]

[DOI]

Vincent Aravantinos

,

,

Nicolas Peltier

Fundam. Informaticae, 2013

An Approach to Abductive Reasoning in Equational Logic.

[BibT_eX]

[DOI]

,

Nicolas Peltier

,

Proceedings of the IJCAI 2013, 2013

2012

An Instantiation Scheme for Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

,

Nicolas Peltier

J. Autom. Reason., 2012

A Calculus for Generating Ground Explanations (Technical Report)

[BibT_eX]

[DOI]

,

Nicolas Peltier

CoRR, 2012

A Calculus for Generating Ground Explanations.

[BibT_eX]

[DOI]

,

Nicolas Peltier

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Reasoning on Schemata of Formulæ.

[BibT_eX]

[DOI]

,

Nicolas Peltier

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

2011

Modular instantiation schemes.

[BibT_eX]

[DOI]

,

Nicolas Peltier

Inf. Process. Lett., 2011

Solving Linear Constraints in Elementary Abelian p-Groups of Symmetries

[BibT_eX]

[DOI]

Thierry Boy de la Tour

,

CoRR, 2011

2010

Theory decision by decomposition.

[BibT_eX]

[DOI]

Maria Paola Bonacina

,

J. Symb. Comput., 2010

Instantiation of SMT Problems Modulo Integers.

[BibT_eX]

[DOI]

,

Nicolas Peltier

Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

2008

On Variable-inactivity and Polynomial tau-Satisfiability Procedures.

[BibT_eX]

[DOI]

Maria Paola Bonacina

,

J. Log. Comput., 2008

Unification and Matching Modulo Leaf-Permutative Equational Presentations.

[BibT_eX]

[DOI]

Thierry Boy de la Tour

,

,

Paliath Narendran

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007

Permutative rewriting and unification.

[BibT_eX]

[DOI]

Thierry Boy de la Tour

,

Inf. Comput., 2007

Determining Unify-Stable Presentations.

[BibT_eX]

[DOI]

Thierry Boy de la Tour

,

Proceedings of the Term Rewriting and Applications, 18th International Conference, 2007

T-Decision by Decomposition.

[BibT_eX]

[DOI]

Maria Paola Bonacina

,

Proceedings of the Automated Deduction, 2007

2006

Rewrite-Based Decision Procedures.

[BibT_eX]

[DOI]

Maria Paola Bonacina

,

Proceedings of the 6th International Workshop on Strategies in Automated Deduction, 2006

Rewrite-Based Satisfiability Procedures for Recursive Data Structures.

[BibT_eX]

[DOI]

Maria Paola Bonacina

,

Proceedings of the Combined Proceedings of the Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2006) and the First International Workshop on Probabilistic Automata and Logics (PaUL 2006), 2006

2005

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

[BibT_eX]

[DOI]

PhD thesis, 2005

Unification in a Class of Permutative Theories.

[BibT_eX]

[DOI]

Thierry Boy de la Tour

,

Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

2004

On the Complexity of Deduction Modulo Leaf Permutative Equations.

[BibT_eX]

[DOI]

Thierry Boy de la Tour

,

J. Autom. Reason., 2004

Overlapping Leaf Permutative Equations.

[BibT_eX]

[DOI]

Thierry Boy de la Tour

,

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003

On Leaf Permutative Theories and Occurrence Permutation Groups.

[BibT_eX]

[DOI]

Thierry Boy de la Tour

,

Proceedings of the 4th International Workshop on First-Order Theorem Proving, 2003

NP-Completeness Results for Deductive Problems on Stratified Terms.

[BibT_eX]

[DOI]

Thierry Boy de la Tour

,

Proceedings of the Logic for Programming, 2003

Loading...