Nombre de documents

55

Publications de 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.

 


Article dans une revue18 documents

  • 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〉
  • 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. 〈http://link.springer.com/article/10.1007/s10817-015-9344-2〉. 〈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〉
  • Nicolas Peltier. A Variant of the Superposition Calculus.. Archive of Formal Proofs, 2016. 〈hal-01383903〉
  • Nicolas Peltier. Tractable and intractable classes of propositional schemata. Journal of Logic and Computation, Oxford University Press (OUP), 2014, 24 (5), pp.111-1139. 〈http://logcom.oxfordjournals.org/content/early/2014/03/14/logcom.exu013.abstract〉. 〈10.1093/logcom/exu013〉. 〈hal-01074412〉
  • Nicolas Peltier. Tractable and intractable classes of propositional schemata. Journal of Logic and Computation, Oxford University Press (OUP), 2014, 24 (5), pp.1111--1139. 〈hal-01132795〉
  • Hicham Bensaid, Nicolas Peltier. A Complete Superposition Calculus for Primal Grammars. Journal of Automated Reasoning, Springer Verlag, 2014, 53 (4), pp.317-350. 〈hal-01132792〉
  • 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〉
  • 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. 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〉
  • 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〉
  • 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〉
  • 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〉
  • 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〉

Communication dans un congrès26 documents

  • Nicolas Peltier, Mnacho Echenim. The Binomial Pricing Model in Finance: A Formalization in Isabelle. Leonardo de Moura. CADE 26, 2017, Gothenburg, Sweden. Springer, 10395, pp.546-562, 2017, 26th International Conference on Automated Deduction. 〈hal-01562944〉
  • Nicolas Peltier. Reasoning on Schemas of Formulas: An Automata-Based Approach. LATA 2015, Mar 2015, Nice, France. Springer, 8977, pp.263-274, Language and Automata Theory and Applications - 9th International Conference. 〈hal-01132791〉
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. Quantifier-Free Equational Logic and Prime Implicate Generation. Amy P. Felty and Aart Middeldorp. CADE-25, Jul 2015, Berlin, Germany. Springer, 9195, pp.311-325, 2015, 25th International Conference on Automated Deduction. 〈10.1007/978-3-319-21401-6_21〉. 〈hal-01363987〉
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. A Rewriting Strategy to Generate Prime Implicates in Equational Logic. IJCAR 2014, Jul 2014, Vienna, Austria. Springer, 8562, pp.137-151, 2014, Automated Reasoning - 7th International Joint Conference. 〈hal-01132797〉
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. A Superposition-Based Approach to Abductive Reasoning in Equational Clausal Logic. ADDTC 2014, Jul 2014, Vienna, Austria. 2014, Automated Deduction: Decidability, Complexity, Tractability. 〈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. 4th Workshop on Practical Aspects of Automated Reasoning. 〈hal-01132801〉
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. A Rewriting Strategy to Generate Prime Implicates in Equational Logic. Stéphane Demri, Deepak Kapur and Christoph Weidenbach. IJCAR 2014, Jul 2014, Vienna, Austria. Springer, 8562, pp.137-151, 2014, Lecture Notes in Computer Science. 〈hal-01018692〉
  • Abdelkader Kersani, Nicolas Peltier. Completeness and Decidability Results for First-order Clauses with Indices. Maria Paola Bonacina. CADE 2013 - 24th International Conference on Automated Deduction, Jun 2013, Lake Placid, NY, United States. Springer, 7898, pp.58-75, 2013, Lecture Notes in Computer Science (LNCS). 〈10.1007/978-3-642-38574-2_4〉. 〈hal-00934594〉
  • Abdelkader Kersani, Nicolas Peltier. Combining Superposition and Induction: A Practical Realization. Fontaine, Pascal and Ringeissen, Christophe and Schmidt, Renate A. FroCoS 2013 - 9th International Symposium on s of Combining Systems (co-located with TABLEAUX 2013), Sep 2013, Nancy, France. Springer, 8152, pp.7-22, 2013, Lecture Notes in Computer Science (LNCS). 〈10.1007/978-3-642-40885-4_2〉. 〈hal-00934610〉
  • Nicolas Peltier. Schemata of Formulæ in the Theory of Arrays. Didier Galmiche, Dominique Larchey-Wendling. TABLEAUX 2013 - 22th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2013, Nancy, France. Springer, 8123, pp.234-249, 2013, Lecture Notes in Computer Science (LNCS). 〈10.1007/978-3-642-40537-2_20〉. 〈hal-00934604〉
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. An Approach to Abductive Reasoning in Equational Logic. Francesca Rossi. IJCAI 2013 - International Joint Conference on Artificial Intelligence, Aug 2013, Beijing, China. AAAI Press, pp.531-537, 2013. 〈hal-00934278〉
  • Mnacho Echenim, Nicolas Peltier. A Calculus for Generating Ground Explanations. Bernhard Gramlich, Dale Miller, Uli Sattler. IJCAR 2012 - International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. Springer, pp.194-209, 2012, Lecture Notes in Computer Science (LNCS). 〈10.1007/978-3-642-31365-3_17〉. 〈hal-00933272〉
  • Mnacho Echenim, Nicolas Peltier. Reasoning on Schemata of Formulæ. Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, Volker Sorge. AISC 2012 - Artificial Intelligence and Symbolic Computation (Part of CICM 2012), Jul 2012, Bremen, Germany. Springer, 7362, pp.310-325, 2012, Lecture Notes in Computer Science (LNCS). 〈10.1007/978-3-642-31374-5_21〉. 〈hal-00933516〉
  • Mnacho Echenim, Nicolas Peltier, Sophie Tourret. A Superposition Strategy for Abductive Reasoning in Ground Equational Logic. Maria Paola Bonacina and Maribel Fern andez. IWS 2012 - International Workshop on Strategies in Rewriting, Proving and Programming (IJCAR 2012 workshop ), Jul 2012, Manchester, United Kingdom. pp.4-11, 2012. 〈hal-00933582〉
  • Vincent Aravantinos, Nicolas Peltier. Generating Schemata of Resolution Proofs. Martin Giese and Roman Kuznets. FTP 2011 - 8th International Workshop on First-Order Theorem Proving (co-located with TABLEAUX 2011), Jul 2011, Bern, Germany. pp.16-30, 2011, Technical Report IAM-11-002. 〈hal-00931720〉
  • 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. IEEE Computer Society, pp.80-87, 2011, 〈10.1109/TIME.2011.11〉. 〈hal-00931690〉
  • Vincent Aravantinos, Nicolas Peltier. Schemata of SMT problems. Kai Brünnler, George Metcalfe. TABLEAUX 2011 - International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Jul 2011, Bern, Switzerland. Springer, 6793, pp.27-42, 2011, Lecture Notes in Computer Science (LNCS). 〈10.1007/978-3-642-22119-4_5〉. 〈hal-00931443〉
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. Complexity of the Satisfiability Problem for a Class of Propositional Schemata. Dediu, Adrian-Horia and Fernau, Henning and Martín-Vide, Carlos. International Conference on Language and Automata Theory and Applications, 2010, Germany. Springer Berlin Heidelberg, 6031, pp.58-69, 2010, Lecture Notes in Computer Science. 〈hal-00940622〉
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. A Decidable Class of Nested Iterated Schemata. Giesl, Jürgen and Hähnle, Reiner. IJCAR 2010, 2010, France. Springer Berlin Heidelberg, 6173, pp.293-308, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-14203-1_25〉. 〈hal-00940623〉
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. RegSTAB: a SAT-Solver for Propositional Schemata. Giesl, Jürgen and Hähnle, Reiner. IJCAR 2010, 2010, Edinburgh, United Kingdom. Springer Berlin Heidelberg, 6173, pp.309-315, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-14203-1_26〉. 〈hal-00940666〉
  • Mnacho Echenim, Nicolas Peltier. Instantiation of SMT Problems Modulo Integers. Autexier, Serge and Calmet, Jacques and Delahaye, David and Ion, PatrickD.F. and Rideau, Laurence and Rioboo, Renaud and Sexton, AlanP. International Conference on Artificial Intelligence and Symbolic Computation, 2010, Paris, France. Springer Berlin Heidelberg, 6167, pp.49-63, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-14128-7_6〉. 〈hal-00940668〉
  • Hicham Bensaid, Ricardo Caferra, Nicolas Peltier. Perfect Discrimination Graphs: Indexing Terms with Integer Exponents. Giesl, Jürgen and Hähnle, Reiner. IJCAR 2010, 2010, Edinburgh, United Kingdom. Springer Berlin Heidelberg, 6173, pp.369-383, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-14203-1_32〉. 〈hal-00940667〉
  • Hicham Bensaid, Ricardo Caferra, Nicolas Peltier. I-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness. Autexier, Serge and Calmet, Jacques and Delahaye, David and Ion, PatrickD.F. and Rideau, Laurence and Rioboo, Renaud and Sexton, AlanP. 10th International Conference on Artificial Intelligence and Symbolic Computation, 2010, Paris, France. Springer Berlin Heidelberg, 6167, pp.19-33, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-14128-7_4〉. 〈hal-00940670〉
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. A Schemata Calculus for Propositional Logic. Giese, Martin and Waaler, Arild. Automated Reasoning with Analytic Tableaux and Related Methods, 18th International Conference, TABLEAUX 2009, 2009, Oslo, Norway. Springer Berlin Heidelberg, 5607, pp.32-46, 2009, Lecture Notes in Computer Science. 〈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. Schmidt, RenateA. 22nd International Conference on Automated Deduction, 2009, Montreal, Canada. Springer Berlin Heidelberg, 5663, pp.146-150, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02959-2_11〉. 〈hal-00940672〉
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. A DPLL Proof Procedure for Propositional Iterated Schemata. Michel Parigot and Lutz Straßburger. ESSLLI'09 Workshop Structures and Deduction, 2009, Bordeaux, France. pp.24, 2009, Research report. 〈hal-00940673〉

Chapitre d'ouvrage2 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〉

Autre publication1 document

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

Pré-publication, Document de travail2 documents

  • Mnacho Echenim, Nicolas Peltier. Instantiation of SMT problems modulo Integers. Research report, long version of our AISC 2010 paper. 2010. 〈hal-00940677〉
  • Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier. A Decidable Class of Nested Iterated Schemata (extended version). 43 pages, extended version of "A Decidable Class of Nested Iterated Schemata". 2010. 〈hal-00940675〉

Rapport5 documents

  • 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, Ricardo Caferra, Nicolas Peltier. Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version). 2011. 〈hal-00932849〉
  • Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier. A Resolution Calculus for Propositional Schemata. 2011. 〈hal-00932855〉
  • Rachid Echahed, Nicolas Peltier. Priority-Independent Rewrite Systems for Pointer-based Data-Structures. 2010. 〈hal-00940674〉

Thèse1 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〉