Nicolas Peltier

According to our database, Nicolas Peltier authored at least 131 papers between 1994 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Some techniques for reasoning automatically on co-inductive data structures.

Nicolas Peltier

J. Log. Comput., 2024

An EXPTIME-Complete Entailment Problem in Separation Logic.

Nicolas Peltier

Proceedings of the Logic, Language, Information, and Computation, 2024

What Is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment?

Tanguy Bozec, Nicolas Peltier, Quentin Petitjean, Mihaela Sighireanu

Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

2023

A Proof Procedure for Separation Logic with Inductive Definitions and Data.

Mnacho Echenim, Nicolas Peltier

J. Autom. Reason., September, 2023

An undecidability result for Separation Logic with theory reasoning.

Mnacho Echenim, Nicolas Peltier

Inf. Process. Lett., August, 2023

Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates.

Mnacho Echenim, Nicolas Peltier

CoRR, 2023

Testing the Satisfiability of Formulas in Separation Logic with Permissions.

Nicolas Peltier

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2023

A Strict Constrained Superposition Calculus for Graphs.

Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier

Proceedings of the Foundations of Software Science and Computation Structures, 2023

2022

Special Issue of Selected Extended Papers of IJCAR 2020.

Nicolas Peltier, Viorica Sofronie-Stokkermans

J. Autom. Reason., 2022

Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules.

Mnacho Echenim, Radu Iosif, Nicolas Peltier

Inf. Process. Lett., 2022

Two Results on Separation Logic With Theory Reasoning.

Mnacho Echenim, Nicolas Peltier

CoRR, 2022

A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning.

Mnacho Echenim, Nicolas Peltier

CoRR, 2022

Reasoning on Dynamic Transformations of Symbolic Heaps.

Nicolas Peltier

Proceedings of the 29th International Symposium on Temporal Representation and Reasoning, 2022

2021

A Superposition-Based Calculus for Quantum Diagrammatic Reasoning and Beyond.

Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier

CoRR, 2021

A Superposition-Based Calculus for Diagrammatic Reasoning.

Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier

Proceedings of the PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming, 2021

Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment.

Mnacho Echenim, Radu Iosif, Nicolas Peltier

Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, 2021

Unifying Decidable Entailments in Separation Logic with Inductive Definitions.

Mnacho Echenim, Radu Iosif, Nicolas Peltier

Proceedings of the Automated Deduction - CADE 28, 2021

2020

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates.

Mnacho Echenim, Radu Iosif, Nicolas Peltier

ACM Trans. Comput. Log., 2020

Combining Induction and Saturation-Based Theorem Proving.

Mnacho Echenim, Nicolas Peltier

J. Autom. Reason., 2020

Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL.

Mnacho Echenim, Hervé Guiol, Nicolas Peltier

J. Autom. Reason., 2020

Checking Entailment Between Separation Logic Symbolic Heaps: Beyond Connected and Established Systems.

Mnacho Echenim, Radu Iosif, Nicolas Peltier

CoRR, 2020

Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems.

Mnacho Echenim, Radu Iosif, Nicolas Peltier

CoRR, 2020

Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard.

Mnacho Echenim, Radu Iosif, Nicolas Peltier

Proceedings of the LPAR 2020: 23rd International Conference on Logic for Programming, 2020

Automated Deduction.

Thierry Boy de la Tour, Ricardo Caferra, Nicola Olivetti, Nicolas Peltier, Camilla Schwind

Proceedings of the A Guided Tour of Artificial Intelligence Research: Volume II: AI Algorithms, 2020

2019

Prenex Separation Logic with One Selector Field.

Mnacho Echenim, Radu Iosif, Nicolas Peltier

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2019

Ilinva: Using Abduction to Generate Loop Invariants.

Mnacho Echenim, Nicolas Peltier, Yanis Sellami

Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains.

Mnacho Echenim, Radu Iosif, Nicolas Peltier

Proceedings of the Foundations of Software Science and Computation Structures, 2019

2018

The Complexity of Prenex Separation Logic with One Selector.

Mnacho Echenim, Radu Iosif, Nicolas Peltier

CoRR, 2018

On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic.

Mnacho Echenim, Radu Iosif, Nicolas Peltier

CoRR, 2018

Prime Implicate Generation in Equational Logic (extended abstract).

Mnacho Echenim, Nicolas Peltier, Sophie Tourret

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018

A Tableaux Calculus for Reducing Proof Size.

Michael Peter Lettmann, Nicolas Peltier

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

A Generic Framework for Implicate Generation Modulo Theories.

Mnacho Echenim, Nicolas Peltier, Yanis Sellami

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

Superposition with Datatypes and Codatatypes.

Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules.

Nicolas Peltier

J. Log. Comput., 2017

CERES for first-order schemata.

Alexander Leitsch, Nicolas Peltier, Daniel Weller

J. Log. Comput., 2017

Prime Implicate Generation in Equational Logic.

Mnacho Echenim, Nicolas Peltier, Sophie Tourret

J. Artif. Intell. Res., 2017

The Binomial Pricing Model in Finance: A Formalization in Isabelle.

Mnacho Echenim, Nicolas Peltier

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Proof Generalization in $$\mathrm {LK}$$ LK by Second Order Unifier Minimization.

Thierry Boy de la Tour, Nicolas Peltier

J. Autom. Reason., 2016

A Superposition Calculus for Abductive Reasoning.

Mnacho Echenim, Nicolas Peltier

J. Autom. Reason., 2016

A Variant of the Superposition Calculus.

Nicolas Peltier

Arch. Formal Proofs, 2016

Propositional Resolution and Prime Implicates Generation.

Nicolas Peltier

Arch. Formal Proofs, 2016

2015

Reasoning on Schemas of Formulas: An Automata-Based Approach.

Nicolas Peltier

Proceedings of the Language and Automata Theory and Applications, 2015

A simulation framework for rapid prototyping and evaluation of thermal mitigation techniques in many-core architectures.

Tanguy Sassolas, Chiara Sandionigi, Alexandre Guerre, Julien Mottin, Pascal Vivet, Hela Boussetta, Nicolas Peltier

Proceedings of the IEEE/ACM International Symposium on Low Power Electronics and Design, 2015

Quantifier-Free Equational Logic and Prime Implicate Generation.

Mnacho Echenim, Nicolas Peltier, Sophie Tourret

Proceedings of the Automated Deduction - CADE-25, 2015

2014

Analogy in Automated Deduction: A Survey.

Thierry Boy de la Tour, Nicolas Peltier

Proceedings of the Computational Approaches to Analogical Reasoning: Current Trends, 2014

Tractable and intractable classes of propositional schemata.

Nicolas Peltier

J. Log. Comput., 2014

A Complete Superposition Calculus for Primal Grammars.

Hicham Bensaid, Nicolas Peltier

J. Autom. Reason., 2014

Early design stage thermal evaluation and mitigation: The locomotiv architectural case.

Tanguy Sassolas, Chiara Sandionigi, Alexandre Guerre, Alexandre Aminot, Pascal Vivet, Hela Boussetta, Luca Ferro, Nicolas Peltier

Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2014

Thermal modeling methodology for efficient system-level thermal analysis.

Cristiano Santos, Pascal Vivet, Gene Matter, Nicolas Peltier, Sylvian Kaiser, Ricardo Augusto da Luz Reis

Proceedings of the IEEE 2014 Custom Integrated Circuits Conference, 2014

A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses.

Sophie Tourret, Mnacho Echenim, Nicolas Peltier

Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

A Rewriting Strategy to Generate Prime Implicates in Equational Logic.

Mnacho Echenim, Nicolas Peltier, Sophie Tourret

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Instantiation Schemes for Nested Theories.

Mnacho Echenim, Nicolas Peltier

ACM Trans. Comput. Log., 2013

A Resolution Calculus for First-order Schemata.

Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier

Fundam. Informaticae, 2013

Schemata of Formulæ in the Theory of Arrays.

Nicolas Peltier

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2013

An Approach to Abductive Reasoning in Equational Logic.

Mnacho Echenim, Nicolas Peltier, Sophie Tourret

Proceedings of the IJCAI 2013, 2013

Combining Superposition and Induction: A Practical Realization.

Abdelkader Kersani, Nicolas Peltier

Proceedings of the Frontiers of Combining Systems, 2013

Completeness and Decidability Results for First-Order Clauses with Indices.

Abdelkader Kersani, Nicolas Peltier

Proceedings of the Automated Deduction - CADE-24, 2013

System-level thermal modeling for 3D circuits: Characterization with a 65nm memory-on-logic circuit.

Cristiano Santos, Pascal Vivet, Denis Dutoit, Philippe Garrault, Nicolas Peltier, Ricardo Reis

Proceedings of the 2013 IEEE International 3D Systems Integration Conference (3DIC), 2013

2012

First-order theorem proving: Foreword.

Nicolas Peltier, Viorica Sofronie-Stokkermans

J. Symb. Comput., 2012

An Instantiation Scheme for Satisfiability Modulo Theories.

Mnacho Echenim, Nicolas Peltier

J. Autom. Reason., 2012

A Calculus for Generating Ground Explanations (Technical Report)

Mnacho Echenim, Nicolas Peltier

CoRR, 2012

A Calculus for Generating Ground Explanations.

Mnacho Echenim, Nicolas Peltier

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Reasoning on Schemata of Formulæ.

Mnacho Echenim, Nicolas Peltier

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

2011

Decidability and Undecidability Results for Propositional Schemata.

Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier

J. Artif. Intell. Res., 2011

Modular instantiation schemes.

Mnacho Echenim, Nicolas Peltier

Inf. Process. Lett., 2011

Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version)

Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier

CoRR, 2011

Linear Temporal Logic and Propositional Schemata, Back and Forth.

Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier

Proceedings of the Eighteenth International Symposium on Temporal Representation and Reasoning, 2011

Generating Schemata of Resolution Proofs.

Vincent Aravantinos, Nicolas Peltier

Proceedings of the TABLEAUX 2011, 2011

Schemata of SMT-Problems.

Vincent Aravantinos, Nicolas Peltier

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2011

2010

Bottom-up Construction of Semantic Tableaux.

Nicolas Peltier

J. Log. Comput., 2010

A Decidable Class of Nested Iterated Schemata (extended version)

Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier

CoRR, 2010

Simplified handling of iterated term schemata.

Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier

Ann. Math. Artif. Intell., 2010

Complexity of the Satisfiability Problem for a Class of Propositional Schemata.

Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier

Proceedings of the Language and Automata Theory and Applications, 2010

Perfect Discrimination Graphs: Indexing Terms with Integer Exponents.

Hicham Bensaid, Ricardo Caferra, Nicolas Peltier

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

RegSTAB: A SAT Solver for Propositional Schemata.

Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

A Decidable Class of Nested Iterated Schemata.

Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

Instantiation of SMT Problems Modulo Integers.

Mnacho Echenim, Nicolas Peltier

Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

<i>I</i>-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness.

Hicham Bensaid, Ricardo Caferra, Nicolas Peltier

Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

2009

Constructing infinite models represented by tree automata.

Nicolas Peltier

Ann. Math. Artif. Intell., 2009

A Schemata Calculus for Propositional Logic.

Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2009

Preface.

Nicolas Peltier, Viorica Sofronie-Stokkermans

Proceedings of the 7th International Workshop on First-Order Theorem Proving, 2009

Dei: A Theorem Prover for Terms with Integer Exponents.

Hicham Bensaid, Ricardo Caferra, Nicolas Peltier

Proceedings of the Automated Deduction, 2009

2008

Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview.

Ricardo Caferra, Nicolas Peltier

Int. J. Intell. Syst., 2008

Extended resolution simulates binary decision diagrams.

Nicolas Peltier

Discret. Appl. Math., 2008

A Needed Rewriting Strategy for Data-Structures with Pointers.

Rachid Echahed, Nicolas Peltier

Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

More Flexible Term Schematisations via Extended Primal Grammars.

Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier

Proceedings of the International Symposium on Artificial Intelligence and Mathematics, 2008

A Unified View of Tree Automata and Term Schematisations.

Nicolas Peltier

Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science, 2008

Automated Model Building: From Finite to Infinite Models.

Nicolas Peltier

Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

2007

A Resolution Calculus with Shared Literals.

Nicolas Peltier

Fundam. Informaticae, 2007

Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps.

Hicham Bensaid, Ricardo Caferra, Nicolas Peltier

Proceedings of the Logic, 2007

A Bottom-Up Approach to Clausal Tableaux.

Nicolas Peltier

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2007

Non Strict Confluent Rewrite Systems for Data-Structures with Pointers.

Rachid Echahed, Nicolas Peltier

Proceedings of the Term Rewriting and Applications, 18th International Conference, 2007

2006

Rewriting term-graphs with priority.

Ricardo Caferra, Rachid Echahed, Nicolas Peltier

Proceedings of the 8th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2006

Narrowing Data-Structures with Pointers.

Rachid Echahed, Nicolas Peltier

Proceedings of the Graph Transformations, Third International Conference, 2006

2005

Some Techniques for Proving Termination of the Hyperresolution Calculus.

Nicolas Peltier

J. Autom. Reason., 2005

A Resolution Calculus for Shortening Proofs.

Nicolas Peltier

Log. J. IGPL, 2005

2004

The first order theory of primal grammars is decidable.

Nicolas Peltier

Theor. Comput. Sci., 2004

A Proof Procedure for Functional First Order Logic Programs with Non-Deterministic Lazy Functions and Built-in Predicates.

Nicolas Peltier

J. Funct. Log. Program., 2004

Representing and Building Models for Decidable Subclasses of Equational Clausal Logic.

Nicolas Peltier

J. Autom. Reason., 2004

Some Techniques for Branch-Saturation in Free-Variable Tableaux.

Nicolas Peltier

Proceedings of the Logics in Artificial Intelligence, 9th European Conference, 2004

2003

A calculus combining resolution and enumeration for building finite models.

Nicolas Peltier

J. Symb. Comput., 2003

Model building with ordered resolution: extracting models from saturated clause sets.

Nicolas Peltier

J. Symb. Comput., 2003

Building Infinite Models for Equational Clause Sets: Constructing Non-Ambiguous Formulae.

Nicolas Peltier

Log. J. IGPL, 2003

Extracting models from clause sets saturated under semantic refinements of the resolution rule.

Nicolas Peltier

Inf. Comput., 2003

Constructing Decision Procedures in Equational Clausal Logic.

Nicolas Peltier

Fundam. Informaticae, 2003

A Resolution-based Model Building Algorithm for a Fragment of OCC1N=.

Nicolas Peltier

Proceedings of the 4th International Workshop on First-Order Theorem Proving, 2003

A More Efficient Tableaux Procedure for Simultaneous Search for Refutations and Finite Models.

Nicolas Peltier

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2003

2001

On the decidability of the PVD class with equality.

Nicolas Peltier

Log. J. IGPL, 2001

A General Method for Using Schematizations in Automated Deduction.

Nicolas Peltier

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

2000

Combining Enumeration and Deductive Techniques in order to Increase the Class of Constructible Infinite Models.

Ricardo Caferra, Nicolas Peltier

J. Symb. Comput., 2000

Workshop: Model Computation - Principles, Algorithms, Applications.

Peter Baumgartner, Christian G. Fermüller, Nicolas Peltier, Hantao Zhang

Proceedings of the Automated Deduction, 2000

The Connection Method, Constraints and Model Building.

Ricardo Caferra, Nicolas Peltier

Proceedings of the Intellectics and Computational Logic (to Wolfgang Bibel on the occasion of his 60th birthday), 2000

Emphasizing Human Techniques in Automated Geometry Theorem Proving: A Practical Realization.

Ricardo Caferra, Nicolas Peltier, François Puitg

Proceedings of the Automated Deduction in Geometry, Third International Workshop, 2000

1999

Pruning the Search Space and Extracting More Models in Tableaux.

Nicolas Peltier

Log. J. IGPL, 1999

1998

A New Method for Automated Finite Model Building Exploiting Failures and Symmetries.

Nicolas Peltier

J. Log. Comput., 1998

Semantic Generalizations for Proving and Disproving Conjectures by Analogy.

Gilles Défourneaux, Christophe Bourely, Nicolas Peltier

J. Autom. Reason., 1998

System Description: An Equational Constraints Solver.

Nicolas Peltier

Proceedings of the Automated Deduction, 1998

1997

Nouvelles techniques pour la construction de modèles finis ou infinis en déduction automatique. (New techniques for finite or infinite model building in automated deduction).

Nicolas Peltier

PhD thesis, 1997

Increasing Model Building Capabilities by Constraint Solving on Terms with Integer Exponents.

Nicolas Peltier

J. Symb. Comput., 1997

A New Technique for Verifying and Correcting Logic Programs.

Ricardo Caferra, Nicolas Peltier

J. Autom. Reason., 1997

Tree Automata and Automated Model Building.

Nicolas Peltier

Fundam. Informaticae, 1997

Simplifying and Generalizing Formulae in Tableaux. Pruning the Search Space and Building Models.

Nicolas Peltier

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1997

Analogy and Abduction in Automated Deduction.

Gilles Défourneaux, Nicolas Peltier

Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, 1997

Partial Matching for Analogy Discovery in Proofs and Counter-Examples.

Gilles Défourneaux, Nicolas Peltier

Proceedings of the Automated Deduction, 1997

1996

Building Proofs or Counterexamples by Analogy in a Resoluton Framework.

Christophe Bourely, Gilles Défourneaux, Nicolas Peltier

Proceedings of the Logics in Artificial Intelligence, European Workshop, 1996

A Significant Extension of Logic Programming by Adapting Model Building Rules.

Ricardo Caferra, Nicolas Peltier

Proceedings of the Extensions of Logic Programming, 5th International Workshop, 1996

Disc_Atinf: A General Framework for Implementing Calculi and Strategies.

Christophe Bourely, Nicolas Peltier

Proceedings of the Design and Implementation of Symbolic Computation Systems, 1996

1995

Model Building and Interactive Theory Discovery.

Ricardo Caferra, Nicolas Peltier

Proceedings of the Theorem Proving with Analytic Tableaux and Related Methods, 1995

Extending Semantic Resolution via Automated Model Building: Applications.

Ricardo Caferra, Nicolas Peltier

Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, 1995

Decision Procedures Using Model Building Techniques.

Ricardo Caferra, Nicolas Peltier

Proceedings of the Computer Science Logic, 9th International Workshop, 1995

1994

A Method for Building Models Automatically. Experiments with an Extension of OTTER.

Christophe Bourely, Ricardo Caferra, Nicolas Peltier

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994