Nicolas Peltier

According to our database1, Nicolas Peltier authored at least 127 papers between 1994 and 2023.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

2023
A Proof Procedure for Separation Logic with Inductive Definitions and Data.
J. Autom. Reason., September, 2023

An undecidability result for Separation Logic with theory reasoning.
Inf. Process. Lett., August, 2023

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

Testing the Satisfiability of Formulas in Separation Logic with Permissions.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2023

A Strict Constrained Superposition Calculus for Graphs.
Proceedings of the Foundations of Software Science and Computation Structures, 2023

2022
Special Issue of Selected Extended Papers of IJCAR 2020.
J. Autom. Reason., 2022

Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules.
Inf. Process. Lett., 2022

Two Results on Separation Logic With Theory Reasoning.
CoRR, 2022

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

Reasoning on Dynamic Transformations of Symbolic Heaps.
Proceedings of the 29th International Symposium on Temporal Representation and Reasoning, 2022

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

A Superposition-Based Calculus for Diagrammatic Reasoning.
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.
Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, 2021

Unifying Decidable Entailments in Separation Logic with Inductive Definitions.
Proceedings of the Automated Deduction - CADE 28, 2021

2020
The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates.
ACM Trans. Comput. Log., 2020

Combining Induction and Saturation-Based Theorem Proving.
J. Autom. Reason., 2020

Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL.
J. Autom. Reason., 2020

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

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

Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard.
Proceedings of the LPAR 2020: 23rd International Conference on Logic for Programming, 2020

2019
Prenex Separation Logic with One Selector Field.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2019

Ilinva: Using Abduction to Generate Loop Invariants.
Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains.
Proceedings of the Foundations of Software Science and Computation Structures, 2019

2018
The Complexity of Prenex Separation Logic with One Selector.
CoRR, 2018

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

Prime Implicate Generation in Equational Logic (extended abstract).
Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, 2018

A Tableaux Calculus for Reducing Proof Size.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

A Generic Framework for Implicate Generation Modulo Theories.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

Superposition with Datatypes and Codatatypes.
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.
J. Log. Comput., 2017

CERES for first-order schemata.
J. Log. Comput., 2017

Prime Implicate Generation in Equational Logic.
J. Artif. Intell. Res., 2017

The Binomial Pricing Model in Finance: A Formalization in Isabelle.
Proceedings of the Automated Deduction - CADE 26, 2017

2016
Proof Generalization in $$\mathrm {LK}$$ LK by Second Order Unifier Minimization.
J. Autom. Reason., 2016

A Superposition Calculus for Abductive Reasoning.
J. Autom. Reason., 2016

A Variant of the Superposition Calculus.
Arch. Formal Proofs, 2016

Propositional Resolution and Prime Implicates Generation.
Arch. Formal Proofs, 2016

2015
Reasoning on Schemas of Formulas: An Automata-Based Approach.
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.
Proceedings of the IEEE/ACM International Symposium on Low Power Electronics and Design, 2015

Quantifier-Free Equational Logic and Prime Implicate Generation.
Proceedings of the Automated Deduction - CADE-25, 2015

2014
Analogy in Automated Deduction: A Survey.
Proceedings of the Computational Approaches to Analogical Reasoning: Current Trends, 2014

Tractable and intractable classes of propositional schemata.
J. Log. Comput., 2014

A Complete Superposition Calculus for Primal Grammars.
J. Autom. Reason., 2014

Early design stage thermal evaluation and mitigation: The locomotiv architectural case.
Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2014

Thermal modeling methodology for efficient system-level thermal analysis.
Proceedings of the IEEE 2014 Custom Integrated Circuits Conference, 2014

A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses.
Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

A Rewriting Strategy to Generate Prime Implicates in Equational Logic.
Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013
Instantiation Schemes for Nested Theories.
ACM Trans. Comput. Log., 2013

A Resolution Calculus for First-order Schemata.
Fundam. Informaticae, 2013

Schemata of Formulæ in the Theory of Arrays.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2013

An Approach to Abductive Reasoning in Equational Logic.
Proceedings of the IJCAI 2013, 2013

Combining Superposition and Induction: A Practical Realization.
Proceedings of the Frontiers of Combining Systems, 2013

Completeness and Decidability Results for First-Order Clauses with Indices.
Proceedings of the Automated Deduction - CADE-24, 2013

System-level thermal modeling for 3D circuits: Characterization with a 65nm memory-on-logic circuit.
Proceedings of the 2013 IEEE International 3D Systems Integration Conference (3DIC), 2013

2012
First-order theorem proving: Foreword.
J. Symb. Comput., 2012

An Instantiation Scheme for Satisfiability Modulo Theories.
J. Autom. Reason., 2012

A Calculus for Generating Ground Explanations (Technical Report)
CoRR, 2012

A Calculus for Generating Ground Explanations.
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Reasoning on Schemata of Formulæ.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

2011
Decidability and Undecidability Results for Propositional Schemata.
J. Artif. Intell. Res., 2011

Modular instantiation schemes.
Inf. Process. Lett., 2011

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

Linear Temporal Logic and Propositional Schemata, Back and Forth.
Proceedings of the Eighteenth International Symposium on Temporal Representation and Reasoning, 2011

Generating Schemata of Resolution Proofs.
Proceedings of the TABLEAUX 2011, 2011

Schemata of SMT-Problems.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2011

2010
Bottom-up Construction of Semantic Tableaux.
J. Log. Comput., 2010

A Decidable Class of Nested Iterated Schemata (extended version)
CoRR, 2010

Simplified handling of iterated term schemata.
Ann. Math. Artif. Intell., 2010

Complexity of the Satisfiability Problem for a Class of Propositional Schemata.
Proceedings of the Language and Automata Theory and Applications, 2010

Perfect Discrimination Graphs: Indexing Terms with Integer Exponents.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

RegSTAB: A SAT Solver for Propositional Schemata.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

A Decidable Class of Nested Iterated Schemata.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

Instantiation of SMT Problems Modulo Integers.
Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

<i>I</i>-Terms in Ordered Resolution and Superposition Calculi: Retrieving Lost Completeness.
Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

2009
Constructing infinite models represented by tree automata.
Ann. Math. Artif. Intell., 2009

A Schemata Calculus for Propositional Logic.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2009

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

Dei: A Theorem Prover for Terms with Integer Exponents.
Proceedings of the Automated Deduction, 2009

2008
Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview.
Int. J. Intell. Syst., 2008

Extended resolution simulates binary decision diagrams.
Discret. Appl. Math., 2008

A Needed Rewriting Strategy for Data-Structures with Pointers.
Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

More Flexible Term Schematisations via Extended Primal Grammars.
Proceedings of the International Symposium on Artificial Intelligence and Mathematics, 2008

A Unified View of Tree Automata and Term Schematisations.
Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science, 2008

Automated Model Building: From Finite to Infinite Models.
Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

2007
A Resolution Calculus with Shared Literals.
Fundam. Informaticae, 2007

Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps.
Proceedings of the Logic, 2007

A Bottom-Up Approach to Clausal Tableaux.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2007

Non Strict Confluent Rewrite Systems for Data-Structures with Pointers.
Proceedings of the Term Rewriting and Applications, 18th International Conference, 2007

2006
Rewriting term-graphs with priority.
Proceedings of the 8th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2006

Narrowing Data-Structures with Pointers.
Proceedings of the Graph Transformations, Third International Conference, 2006

2005
Some Techniques for Proving Termination of the Hyperresolution Calculus.
J. Autom. Reason., 2005

A Resolution Calculus for Shortening Proofs.
Log. J. IGPL, 2005

2004
The first order theory of primal grammars is decidable.
Theor. Comput. Sci., 2004

A Proof Procedure for Functional First Order Logic Programs with Non-Deterministic Lazy Functions and Built-in Predicates.
J. Funct. Log. Program., 2004

Representing and Building Models for Decidable Subclasses of Equational Clausal Logic.
J. Autom. Reason., 2004

Some Techniques for Branch-Saturation in Free-Variable Tableaux.
Proceedings of the Logics in Artificial Intelligence, 9th European Conference, 2004

2003
A calculus combining resolution and enumeration for building finite models.
J. Symb. Comput., 2003

Model building with ordered resolution: extracting models from saturated clause sets.
J. Symb. Comput., 2003

Building Infinite Models for Equational Clause Sets: Constructing Non-Ambiguous Formulae.
Log. J. IGPL, 2003

Extracting models from clause sets saturated under semantic refinements of the resolution rule.
Inf. Comput., 2003

Constructing Decision Procedures in Equational Clausal Logic.
Fundam. Informaticae, 2003

A Resolution-based Model Building Algorithm for a Fragment of OCC1N=.
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.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2003

2001
On the decidability of the PVD class with equality.
Log. J. IGPL, 2001

A General Method for Using Schematizations in Automated Deduction.
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.
J. Symb. Comput., 2000

Workshop: Model Computation - Principles, Algorithms, Applications.
Proceedings of the Automated Deduction, 2000

The Connection Method, Constraints and Model Building.
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.
Proceedings of the Automated Deduction in Geometry, Third International Workshop, 2000

1999
Pruning the Search Space and Extracting More Models in Tableaux.
Log. J. IGPL, 1999

1998
A New Method for Automated Finite Model Building Exploiting Failures and Symmetries.
J. Log. Comput., 1998

Semantic Generalizations for Proving and Disproving Conjectures by Analogy.
J. Autom. Reason., 1998

System Description: An Equational Constraints Solver.
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).
PhD thesis, 1997

Increasing Model Building Capabilities by Constraint Solving on Terms with Integer Exponents.
J. Symb. Comput., 1997

A New Technique for Verifying and Correcting Logic Programs.
J. Autom. Reason., 1997

Tree Automata and Automated Model Building.
Fundam. Informaticae, 1997

Simplifying and Generalizing Formulae in Tableaux. Pruning the Search Space and Building Models.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1997

Analogy and Abduction in Automated Deduction.
Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, 1997

Partial Matching for Analogy Discovery in Proofs and Counter-Examples.
Proceedings of the Automated Deduction, 1997

1996
Building Proofs or Counterexamples by Analogy in a Resoluton Framework.
Proceedings of the Logics in Artificial Intelligence, European Workshop, 1996

A Significant Extension of Logic Programming by Adapting Model Building Rules.
Proceedings of the Extensions of Logic Programming, 5th International Workshop, 1996

Disc<sub>Atinf</sub>: A General Framework for Implementing Calculi and Strategies.
Proceedings of the Design and Implementation of Symbolic Computation Systems, 1996

1995
Model Building and Interactive Theory Discovery.
Proceedings of the Theorem Proving with Analytic Tableaux and Related Methods, 1995

Extending Semantic Resolution via Automated Model Building: Applications.
Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, 1995

Decision Procedures Using Model Building Techniques.
Proceedings of the Computer Science Logic, 9th International Workshop, 1995

1994
A Method for Building Models Automatically. Experiments with an Extension of OTTER.
Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994


  Loading...