- titre
- A Proof Procedure For Separation Logic With Inductive Definitions and Data
- auteur
- Mnacho Echenim, Nicolas Peltier
- article
- Journal of Automated Reasoning, 2023, 67 (3), pp.30. ⟨10.1007/s10817-023-09680-4⟩
- titre
- An undecidability result for Separation Logic with theory reasoning
- auteur
- Mnacho Echenim, Nicolas Peltier
- article
- Information Processing Letters, 2023, 182, pp.106359. ⟨10.1016/j.ipl.2023.106359⟩
- titre
- Testing the Satisfiability of Formulas in Separation Logic with Permissions
- auteur
- Nicolas Peltier
- article
- TABLEAUX 2023 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2023, Prague, Czech Republic
- titre
- A Strict Constrained Superposition Calculus for Graphs
- auteur
- Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier
- article
- FOSSACS 2023: 26th International Conference on Foundations of Software Science and Computation Structures, Apr 2023, Paris, France. pp.135-155, ⟨10.1007/978-3-031-30829-1_7⟩
- titre
- A Strict Constrained Superposition Calculus for Graphs
- auteur
- Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier
- article
- FOSSACS 2023: 26th International Conference on Foundations of Software Science and Computation Structures, Apr 2023, Paris, France
- titre
- Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules
- auteur
- Mnacho Echenim, Radu Iosif, Nicolas Peltier
- article
- Information Processing Letters, 2022, 173, pp.106169. ⟨10.1016/j.ipl.2021.106169⟩
- titre
- Entailment is Undecidable for Symbolic Heap Separation Logic Formulae with Non-Established Inductive Rules
- auteur
- Mnacho Echenim, Radu Iosif, Nicolas Peltier
- article
- Information Processing Letters, 2022
- titre
- Reasoning on Dynamic Transformations of Symbolic Heaps
- auteur
- Nicolas Peltier
- article
- TIME 2022 : 29th International Symposium on Temporal Representation and Reasoning (TIME 2022), Nov 2022, online, France. ⟨10.4230/LIPIcs.TIME.2022.7⟩
- titre
- Two Results on Separation Logic With Theory Reasoning
- auteur
- Mnacho Echenim, Nicolas Peltier
- article
- ASL 2022 - Workshop on Advancing Separation Logic, Jul 2022, Haifa, Israel
- titre
- Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment
- auteur
- Mnacho Echenim, Radu Iosif, Nicolas Peltier
- article
- 29th EACSL Annual Conference on Computer Science Logic, Jan 2021, Ljubljana, Slovenia. ⟨10.4230/LIPIcs.CSL.2021.12⟩
- titre
- A Superposition-Based Calculus for Diagrammatic Reasoning
- auteur
- Nicolas Peltier, Mnacho Echenim, Rachid Echahed, Mehdi Mhalla
- article
- PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming, 2021, Tallinn, Estonia. ⟨10.1145/3479394.3479405⟩
- titre
- Unifying Decidable Entailments in Separation Logic with Inductive Definitions
- auteur
- Mnacho Echenim, Radu Iosif, Nicolas Peltier
- article
- CADE 28, 2021, Pittsburgh (virtual), United States. pp.183-199, ⟨10.1007/978-3-030-79876-5_11⟩
- titre
- Formalizing the Cox–Ross–Rubinstein Pricing of European Derivatives in Isabelle/HOL
- auteur
- Mnacho Echenim, Hervé Guiol, Nicolas Peltier
- article
- Journal of Automated Reasoning, 2020, 64 (4), pp.737-765. ⟨10.1007/s10817-019-09528-w⟩
- titre
- Combining Induction and Saturation-Based Theorem Proving
- auteur
- M. Echenim, Nicolas Peltier
- article
- Journal of Automated Reasoning, 2020, 64 (2), pp.253-294. ⟨10.1007/s10817-019-09519-x⟩
- titre
- The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates
- auteur
- Mnacho Echenim, Radu Iosif, Nicolas Peltier
- article
- ACM Transactions on Computational Logic, 2020, 21
- titre
- The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions
- auteur
- Mnacho Echenim, Radu Iosif, Nicolas Peltier
- article
- ADSL 2020 - Workshop on Automated Deduction in Separation Logic, 2020, New Orleans, United States
- titre
- Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard
- auteur
- Mnacho Echenim, Radu Iosif, Nicolas Peltier
- article
- LPAR 2020, 2020, Alicante, Spain. ⟨10.1145/3380809⟩
- titre
- Checking Entailment Between Separation Logic Symbolic Heaps: Beyond Connected and Established Systems
- auteur
- Nicolas Peltier, Radu Iosif, Mnacho Echenim
- article
- [Research Report] VERIMAG/LIG/CNRS. 2020
- titre
- Prenex Separation Logic with One Selector Field
- auteur
- Mnacho Echenim, Radu Iosif, Nicolas Peltier
- article
- Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, 2019, London, United Kingdom. pp.409-427, ⟨10.1007/978-3-030-29026-9_23⟩
- titre
- Ilinva: Using Abduction to Generate Loop Invariants
- auteur
- Mnacho Echenim, Nicolas Peltier, Yanis Sellami
- article
- Frontiers of Combining Systems - 12th International Symposium, 2019, London, United Kingdom. pp.77-93, ⟨10.1007/978-3-030-29007-8_5⟩
- titre
- The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains
- auteur
- Mnacho Echenim, Radu Iosif, Nicolas Peltier
- article
- Foundations of Software Science and Computation Structures (FOSSACS) - 22nd International Conference, 2019, Prague, Czech Republic. pp.242-259, ⟨10.1007/978-3-030-17127-8_14⟩
- titre
- A Generic Framework for Implicate Generation Modulo Theories
- auteur
- Mnacho Echenim, Nicolas Peltier, Yanis Sellami
- article
- IJCAR, Jul 2018, Oxford, United Kingdom
- titre
- Superposition with Datatypes and Codatatypes
- auteur
- Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard
- article
- IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom
- titre
- Prime Implicate Generation in Equational Logic
- auteur
- Mnacho Echenim, Nicolas Peltier, Sophie Tourret
- article
- Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, 2018, Stockholm, Sweden
- titre
- A Tableaux Calculus for Reducing Proof Size
- auteur
- Michael Peter Lettmann, Nicolas Peltier
- article
- Automated Reasoning - 9th International Joint Conference, IJCAR 2018, 2018, Oxford, United Kingdom
- titre
- The Complexity of Prenex Separation Logic with One Selector
- auteur
- Mnacho Echenim, Radu Iosif, Nicolas Peltier
- article
- 2018
- titre
- On the Expressive Completeness of Bernays-Sch\"onfinkel-Ramsey Separation Logic
- auteur
- Mnacho Echenim, Radu Iosif, Nicolas Peltier
- article
- 2018
- titre
- Prime Implicate Generation in Equational Logic
- auteur
- Mnacho Echenim, Nicolas Peltier, Sophie Tourret
- article
- Journal of Artificial Intelligence Research, 2017, 60, pp.827-880
- titre
- CERES for First-Order Schemata
- auteur
- Alexander Leitsch, Nicolas Peltier, Daniel Weller
- article
- Journal of Logic and Computation, 2017, 27 (7), pp.1897-1954. ⟨10.1093/logcom/exx003⟩
- titre
- A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules
- auteur
- Nicolas Peltier
- article
- Journal of Logic and Computation, 2017, 27 (2), pp.549-576
- titre
- The Binomial Pricing Model in Finance: A Formalization in Isabelle
- auteur
- Nicolas Peltier, Mnacho Echenim
- article
- CADE 26, 2017, Gothenburg, Sweden. pp.546-562
- titre
- A Superposition Calculus for Abductive Reasoning
- auteur
- Mnacho Echenim, Nicolas Peltier
- article
- Journal of Automated Reasoning, 2016, 57 (2), pp.97--134
- titre
- A Variant of the Superposition Calculus.
- auteur
- Nicolas Peltier
- article
- Archive of Formal Proofs, 2016
- titre
- Propositional Resolution and Prime Implicates Generation
- auteur
- Nicolas Peltier
- article
- Archive of Formal Proofs, 2016, 2016
- titre
- Proof Generalization in LK by Second Order Unifier Minimization
- auteur
- Thierry Boy de La Tour, Nicolas Peltier
- article
- Journal of Automated Reasoning, 2016, 57 (3), pp.245-280
- titre
- Quantifier-Free Equational Logic and Prime Implicate Generation
- auteur
- Mnacho Echenim, Nicolas Peltier, Sophie Tourret
- article
- CADE-25, Jul 2015, Berlin, Germany. pp.311-325, ⟨10.1007/978-3-319-21401-6_21⟩
- titre
- Reasoning on Schemas of Formulas: An Automata-Based Approach
- auteur
- Nicolas Peltier
- article
- LATA 2015, Mar 2015, Nice, France. pp.263-274
- titre
- A Complete Superposition Calculus for Primal Grammars
- auteur
- Hicham Bensaid, Nicolas Peltier
- article
- Journal of Automated Reasoning, 2014, 53 (4), pp.317-350. ⟨10.1007/s10817-014-9309-x⟩
- titre
- Tractable and intractable classes of propositional schemata
- auteur
- Nicolas Peltier
- article
- Journal of Logic and Computation, 2014, 24 (5), pp.111-1139. ⟨10.1093/logcom/exu013⟩
- titre
- A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
- auteur
- Mnacho Echenim, Nicolas Peltier, Sophie Tourret
- article
- PAAR 2014, Jul 2014, Vienna, Austria
- titre
- A Superposition-Based Approach to Abductive Reasoning in Equational Clausal Logic
- auteur
- Mnacho Echenim, Nicolas Peltier, Sophie Tourret
- article
- ADDTC 2014, Jul 2014, Vienna, Austria
- titre
- A Rewriting Strategy to Generate Prime Implicates in Equational Logic
- auteur
- Mnacho Echenim, Nicolas Peltier, Sophie Tourret
- article
- IJCAR 2014, Jul 2014, Vienna, Austria. pp.137-151
- titre
- Déduction automatique
- auteur
- Thierry Boy de La Tour, Ricardo Caferra, Nicola Olivetti, Nicolas Peltier, Camilla Schwind
- article
- Marquis Pierre, Papini Odile Prade Henri. L'I.A. frontières et Applications -- Volume 2. Algorithmes pour l'intelligence artificielle, Cépaduès éditions, pp.3, 2014
- titre
- Analogy in Automated Deduction - A Survey
- auteur
- Thierry Boy de La Tour, Nicolas Peltier
- article
- Prade, Henri and Richard, Gilles. Computational Approaches to Analogical Reasoning --- Current Trends, Springer-Verlag, pp.103, 2014, Studies in Computational Intelligence
- titre
- A Resolution Calculus for First-order Schemata
- auteur
- Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier
- article
- Fundamenta Informaticae, 2013, 125 (2), pp.101-133. ⟨10.3233/FI-2013-855⟩
- titre
- Instantiation Schemes for Nested Theories
- auteur
- Mnacho Echenim, Nicolas Peltier
- article
- ACM Transactions on Computational Logic, 2013, 14 (2), pp.11:1-33. ⟨10.1145/2480759.2480763⟩
- titre
- Combining Superposition and Induction: A Practical Realization
- auteur
- Abdelkader Kersani, Nicolas Peltier
- article
- FroCoS 2013 - 9th International Symposium on s of Combining Systems (co-located with TABLEAUX 2013), Sep 2013, Nancy, France. pp.7-22, ⟨10.1007/978-3-642-40885-4_2⟩
- titre
- Schemata of Formulæ in the Theory of Arrays
- auteur
- Nicolas Peltier
- article
- TABLEAUX 2013 - 22th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2013, Nancy, France. pp.234-249, ⟨10.1007/978-3-642-40537-2_20⟩
- titre
- An Approach to Abductive Reasoning in Equational Logic
- auteur
- Mnacho Echenim, Nicolas Peltier, Sophie Tourret
- article
- IJCAI 2013 - International Joint Conference on Artificial Intelligence, Aug 2013, Beijing, China. pp.531-537
- titre
- Completeness and Decidability Results for First-order Clauses with Indices
- auteur
- Abdelkader Kersani, Nicolas Peltier
- article
- CADE 2013 - 24th International Conference on Automated Deduction, Jun 2013, Lake Placid, NY, United States. pp.58-75, ⟨10.1007/978-3-642-38574-2_4⟩
- titre
- An Instantiation Scheme for Satisfiability Modulo Theories
- auteur
- Mnacho Echenim, Nicolas Peltier
- article
- Journal of Automated Reasoning, 2012, 48 (3), pp.293-362. ⟨10.1007/s10817-010-9200-3⟩
- titre
- Reasoning on Schemata of Formulæ
- auteur
- Mnacho Echenim, Nicolas Peltier
- article
- AISC 2012 - Artificial Intelligence and Symbolic Computation (Part of CICM 2012), Jul 2012, Bremen, Germany. pp.310-325, ⟨10.1007/978-3-642-31374-5_21⟩
- titre
- A Superposition Strategy for Abductive Reasoning in Ground Equational Logic
- auteur
- Mnacho Echenim, Nicolas Peltier, Sophie Tourret
- article
- IWS 2012 - International Workshop on Strategies in Rewriting, Proving and Programming (IJCAR 2012 workshop ), Jul 2012, Manchester, United Kingdom. pp.4-11
- titre
- A Calculus for Generating Ground Explanations
- auteur
- Mnacho Echenim, Nicolas Peltier
- article
- IJCAR 2012 - International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. pp.194-209, ⟨10.1007/978-3-642-31365-3_17⟩
- titre
- A Calculus for Generating Ground Explanations (Technical Report)
- auteur
- Mnacho Echenim, Nicolas Peltier
- article
- 2012
- titre
- Modular Instantiation Schemes
- auteur
- Mnacho Echenim, Nicolas Peltier
- article
- Information Processing Letters, 2011, 111 (20), pp.989-993. ⟨10.1016/j.ipl.2011.07.003⟩
- titre
- Decidability and Undecidability Results for Propositional Schemata
- auteur
- Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
- article
- Journal of Artificial Intelligence Research, 2011, 40, pp.599-656. ⟨10.1613/jair.3351⟩
- titre
- Linear Temporal Logic and Propositional Schemata, Back and Forth
- auteur
- Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
- article
- TIME 2011 - International Symposium on Temporal Representation and Reasoning, Sep 2011, Lubeck, Germany. pp.80-87, ⟨10.1109/TIME.2011.11⟩
- titre
- Schemata of SMT problems
- auteur
- Vincent Aravantinos, Nicolas Peltier
- article
- TABLEAUX 2011 - International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Jul 2011, Bern, Switzerland. pp.27-42, ⟨10.1007/978-3-642-22119-4_5⟩
- titre
- Generating Schemata of Resolution Proofs
- auteur
- Vincent Aravantinos, Nicolas Peltier
- article
- FTP 2011 - 8th International Workshop on First-Order Theorem Proving (co-located with TABLEAUX 2011), Jul 2011, Bern, Germany. pp.16-30
- titre
- Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version)
- auteur
- Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
- article
- 2011
- titre
- A Resolution Calculus for Propositional Schemata
- auteur
- Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier
- article
- 2011
- titre
- A Resolution Calculus for First-Order Schemata
- auteur
- Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier
- article
- 2011
- titre
- Bottom-up Construction of Semantic Tableaux
- auteur
- Nicolas Peltier
- article
- Journal of Logic and Computation, 2010, 20 (1), http://logcom.oxfordjournals.org/content/20/1/283.short. ⟨10.1093/logcom/exn069⟩
- titre
- Simplified Handling of Iterated Term Schemata
- auteur
- Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
- article
- Annals of Mathematics and Artificial Intelligence, 2010, 58 (3), pp.155-183. ⟨10.1007/s10472-010-9200-3⟩
- titre
- Perfect Discrimination Graphs: Indexing Terms with Integer Exponents
- auteur
- Hicham Bensaid, Ricardo Caferra, Nicolas Peltier
- article
- IJCAR 2010, 2010, Edinburgh, United Kingdom. pp.369-383, ⟨10.1007/978-3-642-14203-1_32⟩
- titre
- Instantiation of SMT Problems Modulo Integers
- auteur
- Mnacho Echenim, Nicolas Peltier
- article
- International Conference on Artificial Intelligence and Symbolic Computation, 2010, Paris, France. pp.49-63, ⟨10.1007/978-3-642-14128-7_6⟩
- titre
- I-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness
- auteur
- Hicham Bensaid, Ricardo Caferra, Nicolas Peltier
- article
- 10th International Conference on Artificial Intelligence and Symbolic Computation, 2010, Paris, France. pp.19-33, ⟨10.1007/978-3-642-14128-7_4⟩
- titre
- A Decidable Class of Nested Iterated Schemata
- auteur
- Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
- article
- IJCAR 2010, 2010, France. pp.293-308, ⟨10.1007/978-3-642-14203-1_25⟩
- titre
- Complexity of the Satisfiability Problem for a Class of Propositional Schemata
- auteur
- Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
- article
- International Conference on Language and Automata Theory and Applications, 2010, Germany. pp.58-69
- titre
- RegSTAB: a SAT-Solver for Propositional Schemata
- auteur
- Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
- article
- IJCAR 2010, 2010, Edinburgh, United Kingdom. pp.309-315, ⟨10.1007/978-3-642-14203-1_26⟩
- titre
- Priority-Independent Rewrite Systems for Pointer-based Data-Structures
- auteur
- Rachid Echahed, Nicolas Peltier
- article
- 2010
- titre
- Instantiation of SMT problems modulo Integers
- auteur
- Mnacho Echenim, Nicolas Peltier
- article
- 2010
- titre
- A Decidable Class of Nested Iterated Schemata (extended version)
- auteur
- Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
- article
- 2010
- titre
- Constructing Infinite Models Represented by Tree Automata
- auteur
- Nicolas Peltier
- article
- Annals of Mathematics and Artificial Intelligence, 2009, 56 (1), pp.65-85. ⟨10.1007/s10472-009-9143-8⟩
- titre
- A DPLL Proof Procedure for Propositional Iterated Schemata
- auteur
- Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
- article
- ESSLLI'09 Workshop Structures and Deduction, 2009, Bordeaux, France. pp.24
- titre
- Dei: A Theorem Prover for Terms with Integer Exponents
- auteur
- Hicham Bensaid, Ricardo Caferra, Nicolas Peltier
- article
- 22nd International Conference on Automated Deduction, 2009, Montreal, Canada. pp.146-150, ⟨10.1007/978-3-642-02959-2_11⟩
- titre
- A Schemata Calculus for Propositional Logic
- auteur
- Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
- article
- Automated Reasoning with Analytic Tableaux and Related Methods, 18th International Conference, TABLEAUX 2009, 2009, Oslo, Norway. pp.32-46, ⟨10.1007/978-3-642-02716-1_4⟩