Nicolas Peltier

Contact

Email: nicolas.peltier@univ-grenoble-alpes.fr
Office: IMAG building, Grenoble - Room 481
150 place du Torrent
38400 Saint Martin d'Hères, France

Research Interests

• Separation Logic
• Superposition calculus
• Inductive theorem proving
• Formalization of proofs in Isabelle

Publications

Conference Papers

2026

1. Peltier, N. On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions. In CSL 2026 (34th EACSL Annual Conference onComputer Science Logic), 2026.

2025

2. Peltier, N., Petitjean, Q. and Sighireanu, M. Deciding Satisfiability for Overlaid Symbolic Heaps. In Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025, Proceedings, pages 80-97, Springer, 2025.
3. Peltier, N. The Satisfiability Problem in a Separation Logic of Relations. In Logic, Language, Information, and Computation - 31th International Workshop, WoLLIC 2025, 2025.

2024

4. Bozec, T., Peltier, N., Petitjean, Q. and Sighireanu, M. What Is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment?. In Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II, 2024.
5. Peltier, N. An EXPTIME-Complete Entailment Problem in Separation Logic. In Logic, Language, Information, and Computation - 30th International Workshop, WoLLIC 2024, Bern, Switzerland, June 10-13, 2024, Proceedings, 2024.

2023

6. Echahed, R., Echenim, M., Mhalla, M. and Peltier, N. A Strict Constrained Superposition Calculus for Graphs. In FOSSACS 2023: 26th International Conference on Foundations of Software Science and Computation Structures, 2023. more.. 
7. Peltier, N. Testing the Satisfiability of Formulas in Separation Logic with Permissions. In Proceeding of Tableaux'2023, Springer, 2023.

2022

8. Peltier, N. Reasoning on Dynamic Transformations of Symbolic Heaps. In TIME 22 - 29th International Symposium on Temporal Representation and Reasoning, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
9. Echenim, M. and Peltier, N. Two Results on Separation Logic With Theory Reasoning. In ASL 22 (Workshop on Advancing Separation Logic), 2022. more.. 

2021

10. Echenim, M., Iosif, R. and Peltier, N. Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment. In 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference), pages 20:1-20:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. doi..  more.. 
11. Echenim, M., Iosif, R. and Peltier, N. Unifying Decidable Entailments in Separation Logic with Inductive Definitions. In Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, pages 183-199, Springer, 2021. doi..  more.. 
12. Echahed, R., Echenim, M., Mhalla, M. and Peltier, N. A Superposition-Based Calculus for Diagrammatic Reasoning. In 23rd International Symposium on Principles and Practice of Declarative Programming, Association for Computing Machinery, 2021.

2020

13. Echenim, M., Iosif, R. and Peltier, N. Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. In LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, 2020.
14. Echenim, M., Iosif, R. and Peltier, N. The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions. In ADSL 2020 (Second Workshop on Automated Deduction for Separation Logics), New Orleans, Louisiana, United States, 2020.

2019

15. Echenim, M., Iosif, R. and Peltier, N. The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. In Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, pages 242-259, Springer, 2019.
16. Echenim, M., Peltier, N. and Sellami, Y. Ilinva: Using Abduction to Generate Loop Invariants. In Frontiers of Combining Systems - 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings, pages 77-93, Springer, 2019.
17. Echenim, M., Iosif, R. and Peltier, N. Prenex Separation Logic with One Selector Field. In Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings, pages 409-427, Springer, 2019.

2018

18. Echenim, M., Peltier, N. and Tourret, S. Prime Implicate Generation in Equational Logic (extended abstract). In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden., pages 5588-5592, ijcai.org, 2018. more.. 
19. Echenim, M., Peltier, N. and Sellami, Y. A Generic Framework for Implicate Generation Modulo Theories. In Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, pages 279-294, Springer, 2018.
20. Lettmann, M. P. and Peltier, N. A Tableaux Calculus for Reducing Proof Size. In Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, pages 64-80, Springer, 2018.
21. Echenim, M., Iosif, R. and Peltier, N. The Complexity of Prenex Separation Logic with One Selector. In ADSL 18 (First Workshop on Automated Deduction for Separation Logics), 2018.

2017

22. Echenim, M. and Peltier, N. The Binomial Pricing Model in Finance: A Formalization in Isabelle. In Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, pages 546-562, Springer, 2017.

2015

23. Peltier, N. Reasoning on Schemas of Formulas: An Automata-Based Approach. In Proceedings of LATA 2015 (9th International Conference on Language and Automata Theory and Applications), pages 263-274, Springer, 2015.
24. Echenim, M., Peltier, N. and Tourret, S. Quantifier-Free Equational Logic and Prime Implicate Generation. In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pages 311-325, 2015.

2014

25. Echenim, M., Peltier, N. and Tourret, S. A Rewriting Strategy to Generate Prime Implicates in Equational Logic. In Proceedings of the International Joint Conference on Automated Reasoning (IJCAR'14), Springer, 2014.
26. Echenim, M., Peltier, N. and Tourret, S. A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses. In 4th Workshop on Practical Aspects of Automated Reasoning, 2014.
27. Echenim, M., Peltier, N. and Tourret, S. A Superposition-Based Approach to Abductive Reasoning in Equational Clausal Logic. In Proceedings of ADDTC 2014 (Automated Deduction: Decidability, Complexity, Tractability), 2014. more.. 

2013

28. Kersani, A. and Peltier, N. Completeness and Decidability Results for First-order Clauses with Indices. In Proceedings of CADE'13 (24th International Conference on Automated Deduction), pages 58-75, Springer, 2013.
29. Echenim, M., Peltier, N. and Tourret, S. An approach to abductive reasoning in equational logic. In Proceedings of IJCAI'13 (International Conference on Artificial Intelligence), pages 3-9, AAAI, 2013.
30. Peltier, N. Schemata of formulae in the theory of arrays. In Proceedings of TABLEAUX'13 (Automated Reasoning with Analytic Tableaux and Related Methods), pages 234-249, Springer, 2013.
31. Kersani, A. and Peltier, N. Combining Superposition and Induction: A Practical Realization. In Proceedings of FROCOS'13 (Frontiers of Combining Systems, pages 7-22, Springer, 2013.

2012

32. Echenim, M. and Peltier, N. A Calculus for Generating Ground Explanations. In Proceedings of the International Joint Conference on Automated Reasoning (IJCAR'12), pages 194-209, Springer LNCS, 2012.
33. Echenim, M. and Peltier, N. Reasoning on Schemata of Formulae. In Proceedings of CICM 2012 (Conferences on Intelligent Computer Mathematics), pages 310-325, Springer LNCS, 2012.
34. Echenim, M., Peltier, N. and Tourret, S. A Superposition Strategy for Abductive Reasoning in Ground Equational Logic. In Proceedings of IWS 2012 (International Workshop on Strategies), 2012.

2011

35. Aravantinos, V. and Peltier, N. Schemata of SMT problems. In TABLEAUX 11 (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), pages 27-42, Springer, 2011.
36. Aravantinos, V., Caferra, R. and Peltier, N. Linear Temporal Logic and Propositional Schemata, Back and Forth. In TIME'2011 (18th International Symposium on Temporal Representation and Reasoning), 2011.
37. Aravantinos, V. and Peltier, N. Generating Schemata of Resolution Proofs. In FTP 2011 (International Workshop onFirst-Order Theorem Proving), 2011.

2010

38. Aravantinos, V., Caferra, R. and Peltier, N. Complexity of the Satisfiability Problem for a Class of Propositional Schemata. In LATA 2010 (Language, Automata Theory and Applications), pages 58-69, Springer, 2010.
39. Aravantinos, V., Caferra, R. and Peltier, N. A Decidable Class of Nested Iterated Schemata. In IJCAR 2010 (International Joint Conference on Automated Reasoning), pages 293-308, Springer, 2010.
40. Aravantinos, V., Caferra, R. and Peltier, N. RegSTAB: a SAT-Solver for Propositional Schemata. In IJCAR 2010 (International Joint Conference on Automated Reasoning), pages 309-315, Springer, 2010.
41. Bensaid, H., Caferra, R. and Peltier, N. Perfect discrimination graphs: indexing terms with integer exponents. In IJCAR 2010 (International Joint Conference on Automated Reasoning), pages 369-383, Springer, 2010.
42. Echenim, M. and Peltier, N. Instantiation of SMT problems modulo Integers. In AISC 2010 (10th International Conference onArtificial Intelligence and Symbolic Computation), pages 49-63, Springer, 2010.
43. Bensaid, H., Caferra, R. and Peltier, N. I-terms in ordered resolution and superposition calculi : retrieving lost completeness. In AISC 2010 (10th International Conference onArtificial Intelligence and Symbolic Computation), pages 19-33, Springer, 2010.

2009

44. Aravantinos, V., Caferra, R. and Peltier, N. A Schemata Calculus For Propositional Logic. In TABLEAUX 09 (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), pages 32-46, Springer, 2009.
45. Aravantinos, V., Caferra, R. and Peltier, N. A DPLL Proof Procedure for Propositional Iterated Schemata. In Workshop ``Structures and Deduction 2009'' (ESSLI), pages 24-38, 2009.
46. Bensaid, H., Caferra, R. and Peltier, N. DEI: A Theorem Prover for Terms with Integer Exponents. In CADE 22 (22nd International Conference on Automated Deduction), pages 146-150, Springer, 2009.

2008

47. Aravantinos, V., Caferra, R. and Peltier, N. More Flexible Term Schematisations via Extended Primal Grammars. In Tenth International Symposium on Artificial Intelligence and Mathematics (ISAIM), 2008.
48. Echahed, R. and Peltier, N. A Needed Rewriting Strategy for Data-Structures with Pointers. In Rewriting Techniques and Applications, 19th International Conference, RTA 2008, pages 63-78, Springer, 2008.
49. Peltier, N. A Unified View of Tree Automata and Term Schematisations. In Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, pages 491-505, Springer, 2008.
50. Peltier, N. Automated Model Building: From Finite to Infinite Models. In 9th International Conference on Artificial Intelligence and Symbolic Computation, pages 155-169, Springer LNCS, 2008.

2007

51. Echahed, R. and Peltier, N. Non Strict Confluent Rewrite Systems for Data-Structures with Pointers. In Proceedings of RTA (Rewriting Techniques and Applications), Springer LNCS 4533, 2007.
52. Peltier, N. A Bottom-up Approach to Clausal Tableaux. In TABLEAUX'07 (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), Springer LNAI 4548, 2007.
53. Bensaid, H., Caferra, R. and Peltier, N. Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps. In Proc. Wollic'07 (Workshop on Logic, Language, Information and Computation), pages 38-52, Springer, 2007.

2006

54. Caferra, R., Echahed, R. and Peltier, N. Rewriting Term-Graphs with Priority. In Proceedings of the Eighth ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, pages 109-120, ACM Press, 2006.
55. Echahed, R. and Peltier, N. Narrowing Data-Structures with Pointers. In Proceedings of ICGT (International Conference of Graph Transformation), Springer LNCS 4178, 2006.

2005

56. Caferra, R., Echahed, R. and Peltier, N. A Graph Clausal Logic. In FTP'05 (International Workshop First-Order Theorem Proving)., pages 85-96, Technical Report, Universit"at Koblenz-Landau., 2005.

2004

57. Peltier, N. Some Techniques for Branch-Saturation in Free-Variable Tableaux. In JELIA'04 (Logics in Artificial Intelligence, Ninth European Conference), Springer LNCS, 2004.

2003

58. Peltier, N. A Resolution-based Model Building Algorithm for a Fragment of OCC1N=. In Electronic Notes in Theoretical Computer Science, Elsevier, 2003.
59. Peltier, N. A Resolution-based Model Building Algorithm for a Fragment of OCC1N=. In FTP'03 (Fourth International Workshop First-Order Theorem Proving), Technical Report DSIC-II/10/03, http://www.dsic.upv.es, 2003.
60. Peltier, N. A more efficient tableau procedure for simultaneous search for refutations and finite models. In TABLEAUX'03 (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), Springer LNAI 2796, 2003.

2001

61. Peltier, N. A General Method for Using Terms Schematizations in Automated Deduction. In Proceedings of the International Joint Conference on Automated Reasoning (IJCAR'01), pages 578-593, Springer LNCS 2083, 2001.

2000

62. Caferra, R. and Peltier, N. The Connection Method, Constraints and Model Building. In Intellectics and Computational Logic, pages 67-84, Kluwer, 2000.
63. Caferra, R., Peltier, N. and Puitg, F. Emphazing human techniques in geometry automated theorem proving:a practical realization. In Workshop on Automated Deduction in Geometry. Zurich, Switzlerland, Springer, LNAI 2061, 2000.
64. Peltier, N. Combining Resolution and Enumeration for Finite Model Building. In FTP'00 (Third International Workshop First-Order Theorem Proving), pages 170-181, Technical Report, Universit"at Koblenz-Landau., 2000.
65. Peltier, N. Model Building with Ordered Resolution. In FTP'00 (Third International Workshop First-Order Theorem Proving)., pages 158-169, Technical Report, Universit"at Koblenz-Landau., 2000.

1998

66. Peltier, N. An equational constraints solver. In Proceedings of CADE-15, pages 119-123, Springer, 1998.

1997

67. Caferra, R. and Peltier, N. Combining inference and disinference rules with enumeration for model building. In Workshop on model-based reasoning. IJCAI'97, 1997.
68. Caferra, R. and Peltier, N. Model building in the cross-roads of consequence and non-consequence relations. In FTP'97 (International Workshop First-Order Theorem Proving). Technical Report RISC-Linz Report Series No. 97-50, page 40-44., 1997.
69. D'efourneaux, G. and Peltier, N. Partial Matching for Analogy Discovery in Proofs and Counter-examples. In Proceedings of CADE 14, Springer LNAI 1249, 1997.
70. D'efourneaux, G. and Peltier, N. Analogy and Abduction in Automated Reasoning. In Proceedings of IJCAI'97, Nagoya, Japan, 1997.
71. Peltier, N. Simplifying formulae in Tableaux. Pruning the search space and building models. In Proceeding of Tableaux'97, pages 313-327, Springer LNAI 1227, 1997.

1996

72. Bourely, C., D'efourneaux, G. and Peltier, N. Building Proofs or Counterexamples by Analogy in a Resolution Framework. In Proceedings of JELIA 96, pages 34-49, Springer LNAI 1126, 1996.
73. Bourely, C. and Peltier, N. DISC-ATINF: a System for Implementing Strategies and Calculi. In Proceeding of DISCO'96, Springer, 1996.
74. Caferra, R. and Peltier, N. A significant extension of logic programming by adapting model buildings rules. In Proc. of Extensions of Logic Programming 96, pages 51-65, Springer, LNAI 1050, 1996.
75. Caferra, R. and Peltier, N. Decision Procedures using Model Building techniques. In Proceeding of Computer Science Logic, CSL'95, pages 130-144, Springer, LNCS 1092, 1996.

1995

76. Caferra, R. and Peltier, N. Model Building and Interactive Theory Discovery. In Proceeding of Tableaux'95, pages 154-168, Springer, 1995.
77. Caferra, R. and Peltier, N. Extending semantic resolution via automated model building: applications. In Proceeding of IJCAI'95, pages 328-334, Morgan Kaufman, 1995.

1994

78. Bourely, Ch., Caferra, R. and Peltier, N. A Method for Building Models Automatically. Experiments with an extension of OTTER. In Proceedings of CADE-12, pages 72-86, Springer LNAI 814, 1994.

Journal Papers

2026

79. Peltier, N. An EXPTIME-complete entailment problem in separation logic. In Journal of Logic and Computation (accepted, to appear), 2026.

2025

80. Echenim, M. and Peltier, N. A Direct Procedure to Test Entailment in a Separation Logic of Relations. In Journal of Automated Reasoning, 69 (2): 10, 2025.
81. Echenim, M. and Peltier, N. Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates. In Fundamenta Informaticae, 194 (1), 2025.

2024

82. Peltier, N. Some techniques for reasoning automatically on co-inductive data structures. In Journal of Logic and Computation, 34 (3): 429-464, 2024.

2023

83. Echenim, M. and Peltier, N. An undecidability result for Separation Logic with theory reasoning. In Information Processing Letters, 182, 2023.
84. Echenim, M. and Peltier, N. A Proof Procedure for Separation Logic with Inductive Definitions and Data. In J. Autom. Reason., 67 (3): 30, 2023. doi..  more.. 

2022

85. Echenim, M., Iosif, R. and Peltier, N. Entailment is Undecidable for Symbolic Heap Separation Logic Formulae with Non-Established Inductive Rules. In Inf. Process. Lett., 173: 106169, 2022. doi..  more.. 

2020

86. Echenim, M. and Peltier, N. Combining Induction and Saturation-Based Theorem Proving. In J. Autom. Reasoning, 64 (2): 253-294, 2020. doi..  more.. 
87. Echenim, M., Guiol, H. and Peltier, N. Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL. In J. Autom. Reasoning, 64 (4): 737-765, 2020.
88. Echenim, M., Iosif, R. and Peltier, N. The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates. In ACM Trans. Comput. Log., 21 (3): 19:1-19:46, 2020.

2017

89. Leitsch, A., Peltier, N. and Weller, D. CERES for First-Order Schemata. In Journal of Logic and Computation, 27 (7): 1897-1954, 2017.
90. Peltier, N. A Paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules. In Journal of Logic and Computation, 27 (2): 549-576, 2017.
91. Echenim, M., Peltier, N. and Tourret, S. Prime Implicate Generation in Equational Logic. In Journal of Artificial Intelligence Research, 60: 827-880, 2017. more.. 

2016

92. Echenim, M. and Peltier, N. A Superposition Calculus for Abductive Reasoning. In Journal of Automated Reasoning, 57 (2): 97-134, 2016. more.. 
93. Peltier, N. Propositional Resolution and Prime Implicates Generation. In Archive of Formal Proofs, 2016. more.. 
94. T., Boy de la T. and Peltier, N. Proof Generalization in LK by Second Order Unifier Minimization. In J. Autom. Reasoning, 57 (3): 245-280, 2016. doi..  more.. 
95. Peltier, N. A Variant of the Superposition Calculus. In Archive of Formal Proofs, 2016. more.. 

2014

96. Peltier, N. Tractable and intractable classes of propositional schemata. In Journal of Logic and Computation, 24 (5): 1111-1139, 2014.
97. Bensaid, H. and Peltier, N. A Complete Superposition Calculus for Primal Grammars. In Journal of Automated Reasoning, 53 (4): 317-350, 2014.

2013

98. Aravantinos, V., Echenim, M. and Peltier, N. A Resolution Calculus for First-Order Schemata. In Fundamenta Informaticae, 125 (2): 101-133, 2013.
99. Echenim, M. and Peltier, N. Instantiation Schemes for Nested Theories. In ACM Transactions on Computational Logic, 14 (2): 11, 2013.

2012

100. Echenim, M. and Peltier, N. An Instantiation Scheme for Satisfiability Modulo Theories. In Journal of Automated Reasoning, 48 (3), 2012. more.. 

2011

101. Aravantinos, V., Caferra, R. and Peltier, N. Decidability and Undecidability Results for Propositional Schemata. In Journal of Artificial Intelligence Research, 40: 599-656, 2011.
102. Echenim, M. and Peltier, N. Modular instantiation schemes. In Information Processing Letters, 111 (20): 989-993, 2011. more.. 

2010

103. Peltier, N. Bottom-up Construction of Semantic Tableaux. In Journal of Logic and Computation, 20 (1), 2010.
104. Aravantinos, V., Caferra, R. and Peltier, N. Simplified Handling of Iterated Term Schemata. In Annals of Mathematics and Artificial Intelligence, 58 (3): 155, 2010.

2009

105. Peltier, N. Constructing Infinite Models Represented By Tree Automata. In Annals of Mathematics and Artificial Intelligence, 56 (1): 65, 2009.

2008

106. Caferra, R., Echahed, R. and Peltier, N. A Term-Graph Clausal Logic: Completeness and Incompleteness Results. In Journal of Applied Non-Classical Logics, 18 (4): 373-411, 2008.
107. Caferra, R. and Peltier, N. Accepting/Rejecting Propositions from Accepted/Rejected Propositions: a Unifying Overview. In International Journal of Intelligent Systems, 23 (10): 999-1020, 2008.
108. Peltier, N. Extended Resolution Simulates Binary Decision Diagrams. In Discrete Applied Mathematics, 156: 825-837, 2008.

2007

109. Peltier, N. A Resolution Calculus with Shared Literals. In Fundamenta Informaticae, 76 (4): 449-480, 2007.

2006

110. Peltier, N. Some Techniques for Proving Termination of the Hyperresolution Calculus. In Journal of Automated Reasoning, 35: 391-427, 2006.

2005

111. Peltier, N. Representing and Building Models for Decidable Subclasses of Equational Clausal Logic. In Journal of Automated Reasoning, 33 (2): 133-170, 2005.
112. Peltier, N. A Resolution Calculus for Shortening Proofs. In Logic Journal of the Interest Group in Pure and Applied Logics, 13: 307-333, 2005.

2004

113. Peltier, N. The First Order Theory of Primal Grammars is Decidable. In Theoretical Computer Science, 323: 267-320, 2004.
114. Peltier, N. A Proof Procedure for Functional First Order Logic Programs with Non-Deterministic Lazy Functions and Built-in Predicates. In Journal of Functional and Logic Programming, 2004 (3), 2004.

2003

115. Peltier, N. A Calculus Combining Resolution and Enumeration for Building Finite Models. In Journal of Symbolic Computation, 36 (1-2): 49-77, 2003.
116. Peltier, N. Model Building with Ordered Resolution: extracting models from saturated clause sets. In Journal of Symbolic Computation, 36 (1-2): 5-48, 2003.
117. Peltier, N. Extracting Models from Clause Sets Saturated under Semantic Refinements of the Resolution Rule. In Information and Computation, 181: 99-130, 2003.
118. Peltier, N. Building Infinite Models for Equational Clause Sets: Constructing Non-Ambiguous Formulae. In Logic Journal of the IGPL, 11 (1): 103-137, 2003.
119. Peltier, N. Constructing decision procedures in equational clausal logic. In Fundamenta Informaticae, 54 (1): 17-65, 2003.

2001

120. Peltier, N. On the decidability of the PVD class with equality. In Logic Journal of the IGPL, 9 (4): 601-624, 2001.

2000

121. Caferra, R. and Peltier, N. Combining Enumeration and Deductive Techniques in order to Increase the Class of Constructible Infinite Models. In Journal of Symbolic Computation, 29: 177-211, 2000.

1999

122. Peltier, N. Pruning the Search Space and Extracting More Models in Tableaux. In Logic Journal of the IGPL, 7 (2): 217-251, 1999.

1998

123. D'efourneaux, G., Bourely, C. and Peltier, N. Semantic Generalizations for Proving and Disproving conjectures by Analogy. In Journal of Automated Reasoning, 20 (1 & 2): 27-45, 1998.
124. Peltier, N. A new method for automated finite model building exploiting failures and symmetries. In Journal of Logic and Computation, 8 (4): 511-543, 1998.

1997

125. Caferra, R. and Peltier, N. A new technique for verifying and correcting logic programs. In Journal of Automated Reasoning, 19 (3): 277-318, 1997.
126. Peltier, N. Increasing the capabilities of Model building by constraint solving with terms with integer exponents. In Journal of Symbolic Computation, 24: 59-101, 1997.
127. Peltier, N. Tree Automata and Automated Model Building. In Fundamenta Informaticae, 30 (1): 59-81, 1997.

Books

2004

128. Caferra, R., Leitsch, A. and Peltier, N. Automated Model Building. Kluwer Academic Publishers, 2004.

Book chapters

2014

129. T., Boy de la T., Caferra, R., Olivetti, N., Peltier, N. and Schwind, C. D'eduction automatique. more.. 
130. T., Boy de la T. and Peltier, N. Analogy in Automated Deduction -- A Survey. more.. 

1998

131. Caferra, R. and Peltier, N. Disinference rules, model building and abduction.

PhD Theses

1997

132. Peltier, N. Nouvelles Techniques pour la Construction de Mod`eles finis ou infinis en D'eduction Automatique. Ph.D. Thesis, Institut National Polytechnique de Grenoble, 1997.

Conference Proceedings

2020

133. Peltier, N. and Sofronie-Stokkermans, V., ed. Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I. doi..  more.. 
134. Peltier, N. and Sofronie-Stokkermans, V., ed. Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II. doi..  more.. 

2010

135. Peltier, N. and Sofronie-Stokkermans, V., ed. Proceedings of the 7th International Workshop on First-Order Theorem Proving, FTP 2009, Oslo, Norway, July 6-7, 2009. more.. 

2000

136. Baumgartner, P., Ferm"uller, C., Peltier, N. and Zhang, H., ed. CADE-17 Workshop on Model Computation - Principles, Algorithms, Applications.

Teaching

• Ensimag:
  • Théorie des Langages I (2014-2022)
  • Théorie des Langages II (2015-2022)
  • Projet Evaluation de Produits Structurés (2015-2017)
  • Réseaux de neurones pour le pricing (2020-2021)
  • Fondements Logiques pour l'Informatique (2020-2025)
• Université Grenoble Alpes:
  • Introduction à la logique (L2, 2017-2018)
  • Analyse syntaxique (L3, 2018)

Conferences

• IJCAR 2026, IJCAR 2024, IJCAR 2022, IJCAR 2020 (PC co-chair), IJCAR 2018, IJCAR 2016, IJCAR 2012, IJCAR 2010
• IJCAI 2026, IJCAI 2025, IJCAI 2024, IJCAI 2023, IJCAI 2022, IJCAI 2021, IJCAI 2019,
• TABLEAUX 2023, TABLEAUX 2019, TABLEAUX 2017, TABLEAUX 2013, TABLEAUX 2009
• ASL 2022, ADSL 2018
• PAAR 2016, PAAR 2014, PAAR 2012
• CADE 2015, CADE 2003
• FTP 2011, FTP 2009 (PC co-chair), FTP 2005, FTP 2007

Projects

• I am the scientific leader of the CAPP group.
• I am or was involved in the following research projects:
  • NARCO. 2022-2026, funded by the ANR (scientific leader, partners: Verimag, LMF, Loria). See Focus Science CNRS for a general audience article.
  • ASAP. 2010-2013, funded by the French National Research Agency and by the Austrian Science Fund. Scientific leader of the French part. Partner: Theory and Logic Group, TU Vienna (A. Leitsch).
  • ARROWS. 2005-2009, funded by the ANR.

Links

• The CNRS
• The Laboratory of Informatics of Grenoble
• The CAPP team - Calculus, Algorithms, Programs and Proofs
• Colleagues and former students
  • V. Aravantinos (PhD 2007-2010)
  • H. Bensaid (PhD, 2008-2011, now associate professor at INPT, Morocco)
  • M. Echenim (Professor at Grenoble INP, Ensimag)
  • R. Iosif (CNRS Senior Researcher, Verimag)
  • Y. Sellami (PhD 2016-2020, now Research Engineer at CEA)
  • M. Sighireanu (Professor, ENS Paris-Saclay)
  • S. Tourret (PhD, 2012-2016, now Researcher at Inria, Nancy).