Mnacho Echenim

Available identifiers

zbMath Open echenim.mnachoMaRDI QIDQ438577

List of research outcomes

Publication	Date of Publication	Type
A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL	2024-02-06	Paper
A strict constrained superposition calculus for graphs	2023-11-24	Paper
A proof procedure for separation logic with inductive definitions and data	2023-10-24	Paper
Unbiasing and robustifying implied volatility calibration in a cryptocurrency market with large bid-ask spreads and missing quotes	2023-09-25	Paper
An undecidability result for separation logic with theory reasoning	2023-06-05	Paper
Unifying decidable entailments in separation logic with inductive definitions	2021-12-01	Paper
Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules	2021-10-19	Paper
The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates	2020-09-11	Paper
Prenex separation logic with one selector field	2020-05-14	Paper
Ilinva: using abduction to generate loop invariants	2020-05-13	Paper
Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL	2020-04-07	Paper
Combining induction and saturation-based theorem proving	2020-03-03	Paper
The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains	2020-01-28	Paper
A generic framework for implicate generation modulo theories	2018-10-18	Paper
Prime Implicate Generation in Equational Logic	2018-01-12	Paper
The binomial pricing model in finance: a formalization in Isabelle	2017-09-22	Paper
A superposition calculus for abductive reasoning	2017-08-17	Paper
Quantifier-Free Equational Logic and Prime Implicate Generation	2015-12-02	Paper
Instantiation Schemes for Nested Theories	2015-09-17	Paper
A Rewriting Strategy to Generate Prime Implicates in Equational Logic	2014-09-26	Paper
Rewrite-based satisfiability procedures for recursive data structures	2013-12-06	Paper
Rewrite-based decision procedures	2013-12-06	Paper
A resolution calculus for first-order schemata	2013-08-26	Paper
On leaf permutative theories and occurrence permutation groups	2013-04-19	Paper
Modular instantiation schemes	2013-04-04	Paper
Reasoning on Schemata of Formulæ	2012-09-07	Paper
A Calculus for Generating Ground Explanations	2012-09-05	Paper
An instantiation scheme for satisfiability modulo theories	2012-07-31	Paper
Instantiation of SMT problems modulo integers	2010-08-24	Paper
NP-completeness results for deductive problems on stratified terms	2010-02-24	Paper
Theory decision by decomposition	2009-12-03	Paper
${\mathcal{T}}$ -Decision by Decomposition	2009-03-06	Paper
Unification and Matching Modulo Leaf-Permutative Equational Presentations	2008-11-27	Paper
On Variable-inactivity and Polynomial Formula-Satisfiability Procedures	2008-03-12	Paper
Determining Unify-Stable Presentations	2008-01-02	Paper
Automated Reasoning	2007-09-25	Paper
Permutative rewriting and unification	2007-04-16	Paper
Term Rewriting and Applications	2005-11-11	Paper
On the complexity of deduction modulo leaf permutative equations	2005-06-22	Paper

Research outcomes over time

This page was built for person: Mnacho Echenim