Skip to Main content
Number of documents

72

Publications of Nicolas Peltier


I am a research scientist in the CNRS. I work in the team CAPP of the LIG (Grenoble Informatics Laboratory).

Please see my web page for more details.

 


Journal articles20 documents

  • M. Echenim, Nicolas Peltier. Combining Induction and Saturation-Based Theorem Proving. Journal of Automated Reasoning, Springer Verlag, 2020, 64 (2), pp.253-294. ⟨10.1007/s10817-019-09519-x⟩. ⟨hal-02990367⟩
  • Mnacho Echenim, Hervé Guiol, Nicolas Peltier. Formalizing the Cox–Ross–Rubinstein Pricing of European Derivatives in Isabelle/HOL. Journal of Automated Reasoning, Springer Verlag, 2020, 64 (4), pp.737-765. ⟨10.1007/s10817-019-09528-w⟩. ⟨hal-02990376⟩
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates. ACM Transactions on Computational Logic, Association for Computing Machinery, In press. ⟨hal-02388326⟩
  • Nicolas Peltier. A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules . Journal of Logic and Computation, Oxford University Press (OUP), 2017, 27 (2), pp.549-576. ⟨hal-01516896⟩
  • Alexander Leitsch, Nicolas Peltier, Daniel Weller. CERES for First-Order Schemata. Journal of Logic and Computation, Oxford University Press (OUP), 2017, 27 (7), pp.1897-1954. ⟨10.1093/logcom/exx003⟩. ⟨hal-01621380⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. Prime Implicate Generation in Equational Logic. Journal of Artificial Intelligence Research, Association for the Advancement of Artificial Intelligence, 2017, 60, pp.827-880. ⟨hal-01946538⟩
  • Nicolas Peltier. A Variant of the Superposition Calculus.. Archive of Formal Proofs, 2016. ⟨hal-01383903⟩
  • Nicolas Peltier. Propositional Resolution and Prime Implicates Generation. Archive of Formal Proofs, 2016, 2016. ⟨hal-01364005⟩
  • Mnacho Echenim, Nicolas Peltier. A Superposition Calculus for Abductive Reasoning. Journal of Automated Reasoning, Springer Verlag, 2016, 57 (2), pp.97--134. ⟨hal-01363997⟩
  • Thierry Boy de la Tour, Nicolas Peltier. Proof Generalization in LK by Second Order Unifier Minimization. Journal of Automated Reasoning, Springer Verlag, 2016, 57 (3), pp.245-280. ⟨hal-01364000⟩
  • Hicham Bensaid, Nicolas Peltier. A Complete Superposition Calculus for Primal Grammars. Journal of Automated Reasoning, Springer Verlag, 2014, 53 (4), pp.317-350. ⟨hal-01083011⟩
  • Nicolas Peltier. Tractable and intractable classes of propositional schemata. Journal of Logic and Computation, Oxford University Press (OUP), 2014, 24 (5), pp.111-1139. ⟨10.1093/logcom/exu013⟩. ⟨hal-01074412⟩
  • Mnacho Echenim, Nicolas Peltier. Instantiation Schemes for Nested Theories. ACM Transactions on Computational Logic, Association for Computing Machinery, 2013, 14 (2), pp.11:1-33. ⟨10.1145/2480759.2480763⟩. ⟨hal-00933873⟩
  • Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier. A Resolution Calculus for First-order Schemata. Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2013, 125 (2), pp.101-133. ⟨10.3233/FI-2013-855⟩. ⟨hal-00933896⟩
  • Mnacho Echenim, Nicolas Peltier. An Instantiation Scheme for Satisfiability Modulo Theories. Journal of Automated Reasoning, Springer Verlag, 2012, 48 (3), pp.293-362. ⟨10.1007/s10817-010-9200-3⟩. ⟨hal-00933247⟩
  • Mnacho Echenim, Nicolas Peltier. Modular Instantiation Schemes. Information Processing Letters, Elsevier, 2011, 111 (20), pp.989-993. ⟨10.1016/j.ipl.2011.07.003⟩. ⟨hal-00931264⟩
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. Decidability and Undecidability Results for Propositional Schemata. Journal of Artificial Intelligence Research, Association for the Advancement of Artificial Intelligence, 2011, 40, pp.599-656. ⟨10.1613/jair.3351⟩. ⟨hal-00931221⟩
  • Nicolas Peltier. Bottom-up Construction of Semantic Tableaux. Journal of Logic and Computation, Oxford University Press (OUP), 2010, 20 (1), http://logcom.oxfordjournals.org/content/20/1/283.short. ⟨10.1093/logcom/exn069⟩. ⟨hal-00940603⟩
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. Simplified Handling of Iterated Term Schemata. Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2010, 58 (3), pp.155-183. ⟨10.1007/s10472-010-9200-3⟩. ⟨hal-00940620⟩
  • Nicolas Peltier. Constructing Infinite Models Represented by Tree Automata. Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2009, 56 (1), pp.65-85. ⟨10.1007/s10472-009-9143-8⟩. ⟨hal-00940621⟩

Conference papers37 documents

  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. LPAR 2020, 2020, Alicante, Spain. ⟨10.1145/3380809⟩. ⟨hal-02990396⟩
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions. ADSL 2020 - Workshop on Automated Deduction in Separation Logic, 2020, New Orleans, United States. ⟨hal-02388028⟩
  • Mnacho Echenim, Nicolas Peltier, Yanis Sellami. Ilinva: Using Abduction to Generate Loop Invariants. Frontiers of Combining Systems - 12th International Symposium, 2019, London, United Kingdom. pp.77-93, ⟨10.1007/978-3-030-29007-8_5⟩. ⟨hal-02323446⟩
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. 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⟩. ⟨hal-02094154⟩
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. Prenex Separation Logic with One Selector Field. 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⟩. ⟨hal-02323468⟩
  • Michael Lettmann, Nicolas Peltier. A Tableaux Calculus for Reducing Proof Size. Automated Reasoning - 9th International Joint Conference, IJCAR 2018, 2018, Oxford, United Kingdom. ⟨hal-01946472⟩
  • Mnacho Echenim, Nicolas Peltier, Yanis Sellami. A Generic Framework for Implicate Generation Modulo Theories. IJCAR, Jul 2018, Oxford, United Kingdom. ⟨hal-01833514⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. Prime Implicate Generation in Equational Logic. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, 2018, Stockholm, Sweden. ⟨hal-01946497⟩
  • Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard. Superposition with Datatypes and Codatatypes. IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. ⟨hal-01904588⟩
  • Nicolas Peltier, Mnacho Echenim. The Binomial Pricing Model in Finance: A Formalization in Isabelle. CADE 26, 2017, Gothenburg, Sweden. pp.546-562. ⟨hal-01562944⟩
  • Tanguy Sassolas, Chiara Sandionigi, Alexandre Guerre, Julien Mottin, Pascal Vivet, et al.. A simulation framework for rapid prototyping and evaluation of thermal mitigation techniques in many-core architectures. 2015 IEEE/ACM International Symposium on Low Power Electronics and Design (ISLPED), Jul 2015, Rome, Italy. ⟨10.1109/ISLPED.2015.7273485⟩. ⟨cea-01235183⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. Quantifier-Free Equational Logic and Prime Implicate Generation. CADE-25, Jul 2015, Berlin, Germany. pp.311-325, ⟨10.1007/978-3-319-21401-6_21⟩. ⟨hal-01363987⟩
  • Nicolas Peltier. Reasoning on Schemas of Formulas: An Automata-Based Approach. LATA 2015, Mar 2015, Nice, France. pp.263-274. ⟨hal-01132791⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. A Superposition-Based Approach to Abductive Reasoning in Equational Clausal Logic. ADDTC 2014, Jul 2014, Vienna, Austria. ⟨hal-01132800⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses. PAAR 2014, Jul 2014, Vienna, Austria. ⟨hal-01132801⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. A Rewriting Strategy to Generate Prime Implicates in Equational Logic. IJCAR 2014, Jul 2014, Vienna, Austria. pp.137-151. ⟨hal-01018692⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. An Approach to Abductive Reasoning in Equational Logic. IJCAI 2013 - International Joint Conference on Artificial Intelligence, Aug 2013, Beijing, China. pp.531-537. ⟨hal-00934278⟩
  • Abdelkader Kersani, Nicolas Peltier. Completeness and Decidability Results for First-order Clauses with Indices. 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⟩. ⟨hal-00934594⟩
  • Nicolas Peltier. Schemata of Formulæ in the Theory of Arrays. 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⟩. ⟨hal-00934604⟩
  • Abdelkader Kersani, Nicolas Peltier. Combining Superposition and Induction: A Practical Realization. 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⟩. ⟨hal-00934610⟩
  • Mnacho Echenim, Nicolas Peltier. A Calculus for Generating Ground Explanations. IJCAR 2012 - International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. pp.194-209, ⟨10.1007/978-3-642-31365-3_17⟩. ⟨hal-00933272⟩
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. A Superposition Strategy for Abductive Reasoning in Ground Equational Logic. IWS 2012 - International Workshop on Strategies in Rewriting, Proving and Programming (IJCAR 2012 workshop ), Jul 2012, Manchester, United Kingdom. pp.4-11. ⟨hal-00933582⟩
  • Mnacho Echenim, Nicolas Peltier. Reasoning on Schemata of Formulæ. 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⟩. ⟨hal-00933516⟩
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. Linear Temporal Logic and Propositional Schemata, Back and Forth. TIME 2011 - International Symposium on Temporal Representation and Reasoning, Sep 2011, Lubeck, Germany. pp.80-87, ⟨10.1109/TIME.2011.11⟩. ⟨hal-00931690⟩
  • Vincent Aravantinos, Nicolas Peltier. Generating Schemata of Resolution Proofs. FTP 2011 - 8th International Workshop on First-Order Theorem Proving (co-located with TABLEAUX 2011), Jul 2011, Bern, Germany. pp.16-30. ⟨hal-00931720⟩
  • Vincent Aravantinos, Nicolas Peltier. Schemata of SMT problems. 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⟩. ⟨hal-00931443⟩
  • Hicham Bensaid, Ricardo Caferra, Nicolas Peltier. Perfect Discrimination Graphs: Indexing Terms with Integer Exponents. IJCAR 2010, 2010, Edinburgh, United Kingdom. pp.369-383, ⟨10.1007/978-3-642-14203-1_32⟩. ⟨hal-00940667⟩
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. Complexity of the Satisfiability Problem for a Class of Propositional Schemata. International Conference on Language and Automata Theory and Applications, 2010, Germany. pp.58-69. ⟨hal-00940622⟩
  • Hicham Bensaid, Ricardo Caferra, Nicolas Peltier. I-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness. 10th International Conference on Artificial Intelligence and Symbolic Computation, 2010, Paris, France. pp.19-33, ⟨10.1007/978-3-642-14128-7_4⟩. ⟨hal-00940670⟩
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. RegSTAB: a SAT-Solver for Propositional Schemata. IJCAR 2010, 2010, Edinburgh, United Kingdom. pp.309-315, ⟨10.1007/978-3-642-14203-1_26⟩. ⟨hal-00940666⟩
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. A Decidable Class of Nested Iterated Schemata. IJCAR 2010, 2010, France. pp.293-308, ⟨10.1007/978-3-642-14203-1_25⟩. ⟨hal-00940623⟩
  • Mnacho Echenim, Nicolas Peltier. Instantiation of SMT Problems Modulo Integers. International Conference on Artificial Intelligence and Symbolic Computation, 2010, Paris, France. pp.49-63, ⟨10.1007/978-3-642-14128-7_6⟩. ⟨hal-00940668⟩
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. A DPLL Proof Procedure for Propositional Iterated Schemata. ESSLLI'09 Workshop Structures and Deduction, 2009, Bordeaux, France. pp.24. ⟨hal-00940673⟩
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. A Schemata Calculus for Propositional Logic. 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⟩. ⟨hal-00940671⟩
  • Hicham Bensaid, Ricardo Caferra, Nicolas Peltier. Dei: A Theorem Prover for Terms with Integer Exponents. 22nd International Conference on Automated Deduction, 2009, Montreal, Canada. pp.146-150, ⟨10.1007/978-3-642-02959-2_11⟩. ⟨hal-00940672⟩
  • Olivier Martins, Nicolas Peltier, Stéphane Guédon, Sylvian Kaiser, Yves Maréchal, et al.. A new Methodology for Multi-Level Thermal Characterization of Complex Electronic Systems: From Die to Board Level. European Microelectronics and Packaging Conference (EMPC 2009), Jun 2009, Rimini, Italy. ⟨hal-00400083⟩
  • Olivier Martins, Nicolas Peltier, Stéphane Guédon, Sylvian Kaiser, Yves Maréchal, et al.. A New Methodology for Early Stage Thermal Analysis of Complex Electronic Systems. Therminic 2009, Oct 2009, Leuven, Belgium. ⟨hal-00423729⟩

Book sections2 documents

  • Thierry Boy de la Tour, Ricardo Caferra, Nicola Olivetti, Nicolas Peltier, Camilla Schwind. Déduction automatique. 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. ⟨hal-00995598⟩
  • Thierry Boy de la Tour, Nicolas Peltier. Analogy in Automated Deduction - A Survey. Prade, Henri and Richard, Gilles. Computational Approaches to Analogical Reasoning --- Current Trends, Springer-Verlag, pp.103, 2014, Studies in Computational Intelligence. ⟨hal-00995596⟩

Other publications1 document

  • Nicolas Balacheff, Ricardo Caferra, Michele Cerulli, Nathalie Gaudin, Mirko Maracci, et al.. Baghera Assessment Project, designing an hybrid and emergent educational society. 2003. ⟨hal-00190323⟩

Preprints, Working Papers, ...5 documents

  • Mnacho Echenim, Herve Guiol, Nicolas Peltier. Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL. 2018. ⟨hal-01954948⟩
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. On the Expressive Completeness of Bernays-Sch\"onfinkel-Ramsey Separation Logic. 2018. ⟨hal-01699151⟩
  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. The Complexity of Prenex Separation Logic with One Selector. 2018. ⟨hal-01946528⟩
  • Mnacho Echenim, Nicolas Peltier. Instantiation of SMT problems modulo Integers. 2010. ⟨hal-00940677⟩
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. A Decidable Class of Nested Iterated Schemata (extended version). 2010. ⟨hal-00940675⟩

Reports6 documents

  • Mnacho Echenim, Radu Iosif, Nicolas Peltier. Entailment is Undecidable for Symbolic Heap Separation Logic Formulae with Non-Established Inductive Rules. [Research Report] CNRS. 2020. ⟨hal-02951859v2⟩
  • Mnacho Echenim, Nicolas Peltier. A Calculus for Generating Ground Explanations (Technical Report). 2012. ⟨hal-00933750⟩
  • Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier. A Resolution Calculus for First-Order Schemata. 2011. ⟨hal-00932856⟩
  • Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier. A Resolution Calculus for Propositional Schemata. 2011. ⟨hal-00932855⟩
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version). 2011. ⟨hal-00932849⟩
  • Rachid Echahed, Nicolas Peltier. Priority-Independent Rewrite Systems for Pointer-based Data-Structures. 2010. ⟨hal-00940674⟩

Theses1 document

  • Nicolas Peltier. Nouvelles techniques pour la construction de modèles finis ou infinis en déduction automatique. Modélisation et simulation. Institut National Polytechnique de Grenoble - INPG, 1997. Français. ⟨tel-00004960⟩