Nicolas Peltier

150 papers A* 3A 20B 18C 9Misc 1Journal 72Unranked 21

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Applying Saturation-Based Theorem Proving to Open Problems in Positive Implicational Logic. J. Autom. Reason. Branden Fitelson, Nicolas Peltier
2026	B	`conf`	On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions. CSL Nicolas Peltier
2025	J	`jnl`	A Direct Procedure to Test Entailment in a Separation Logic of Relations. J. Autom. Reason. Mnacho Echenim, Nicolas Peltier
2025	—	`conf`	Deciding Satisfiability for Overlaid Symbolic Heaps. FroCoS Nicolas Peltier, Quentin Petitjean, Mihaela Sighireanu
2025	C	`conf`	The Satisfiability Problem in a Separation Logic of Relations. WoLLIC Nicolas Peltier
2025	J	`jnl`	Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates. Fundam. Informaticae Mnacho Echenim, Nicolas Peltier
2024	C	`conf`	An EXPTIME-Complete Entailment Problem in Separation Logic. WoLLIC Nicolas Peltier
2024	J	`jnl`	Some techniques for reasoning automatically on co-inductive data structures. J. Log. Comput. Nicolas Peltier
2024	—	`conf`	What Is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment? IJCAR (2) Tanguy Bozec, Nicolas Peltier, Quentin Petitjean, Mihaela Sighireanu
2023	J	`jnl`	A Proof Procedure for Separation Logic with Inductive Definitions and Data. J. Autom. Reason. Mnacho Echenim, Nicolas Peltier
2023	B	`conf`	A Strict Constrained Superposition Calculus for Graphs. FoSSaCS Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier
2023	J	`jnl`	An undecidability result for Separation Logic with theory reasoning. Inf. Process. Lett. Mnacho Echenim, Nicolas Peltier
2023	B	`conf`	Testing the Satisfiability of Formulas in Separation Logic with Permissions. TABLEAUX Nicolas Peltier
2023	J	`jnl`	Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates. CoRR Mnacho Echenim, Nicolas Peltier
2022	J	`jnl`	A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning. CoRR Mnacho Echenim, Nicolas Peltier
2022	J	`jnl`	Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules. Inf. Process. Lett. Mnacho Echenim, Radu Iosif, Nicolas Peltier
2022	C	`conf`	Reasoning on Dynamic Transformations of Symbolic Heaps. TIME Nicolas Peltier
2022	J	`jnl`	Special Issue of Selected Extended Papers of IJCAR 2020. J. Autom. Reason. Nicolas Peltier, Viorica Sofronie-Stokkermans
2022	J	`jnl`	Two Results on Separation Logic With Theory Reasoning. CoRR Mnacho Echenim, Nicolas Peltier
2021	C	`conf`	A Superposition-Based Calculus for Diagrammatic Reasoning. PPDP Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier
2021	J	`jnl`	A Superposition-Based Calculus for Quantum Diagrammatic Reasoning and Beyond. CoRR Rachid Echahed, Mnacho Echenim, Mehdi Mhalla, Nicolas Peltier
2021	B	`conf`	Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment. CSL Mnacho Echenim, Radu Iosif, Nicolas Peltier
2021	A	`conf`	Unifying Decidable Entailments in Separation Logic with Inductive Definitions. CADE Mnacho Echenim, Radu Iosif, Nicolas Peltier
2020	—	`ch.`	Automated Deduction. A Guided Tour of Artificial Intelligence Research (2) (II) Thierry Boy de la Tour, Ricardo Caferra, Nicola Olivetti, Nicolas Peltier, Camilla Schwind
2020	—	`ed.`	Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I IJCAR (1) Nicolas Peltier, Viorica Sofronie-Stokkermans
2020	—	`ed.`	Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II IJCAR (2) Nicolas Peltier, Viorica Sofronie-Stokkermans
2020	J	`jnl`	Checking Entailment Between Separation Logic Symbolic Heaps: Beyond Connected and Established Systems. CoRR Mnacho Echenim, Radu Iosif, Nicolas Peltier
2020	J	`jnl`	Combining Induction and Saturation-Based Theorem Proving. J. Autom. Reason. Mnacho Echenim, Nicolas Peltier
2020	J	`jnl`	Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Established Systems. CoRR Mnacho Echenim, Radu Iosif, Nicolas Peltier
2020	B	`conf`	Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. LPAR Mnacho Echenim, Radu Iosif, Nicolas Peltier
2020	J	`jnl`	Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. CoRR Mnacho Echenim, Radu Iosif, Nicolas Peltier
2020	J	`jnl`	Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL. J. Autom. Reason. Mnacho Echenim, Hervé Guiol, Nicolas Peltier
2020	J	`jnl`	The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates. ACM Trans. Comput. Log. Mnacho Echenim, Radu Iosif, Nicolas Peltier
2019	—	`conf`	Ilinva: Using Abduction to Generate Loop Invariants. FroCos Mnacho Echenim, Nicolas Peltier, Yanis Sellami
2019	J	`jnl`	Ilinva: Using Abduction to Generate Loop Invariants. CoRR Mnacho Echenim, Nicolas Peltier, Yanis Sellami
2019	B	`conf`	Prenex Separation Logic with One Selector Field. TABLEAUX Mnacho Echenim, Radu Iosif, Nicolas Peltier
2019	B	`conf`	The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. FoSSaCS Mnacho Echenim, Radu Iosif, Nicolas Peltier
2018	A	`conf`	A Generic Framework for Implicate Generation Modulo Theories. IJCAR Mnacho Echenim, Nicolas Peltier, Yanis Sellami
2018	J	`jnl`	A Generic Framework for Implicate Generation Modulo Theories. CoRR Mnacho Echenim, Nicolas Peltier, Yanis Sellami
2018	A	`conf`	A Tableaux Calculus for Reducing Proof Size. IJCAR Michael Peter Lettmann, Nicolas Peltier
2018	J	`jnl`	A Tableaux Calculus for Reducing Proof Size. CoRR Michael Peter Lettmann, Nicolas Peltier
2018	J	`jnl`	Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL. CoRR Mnacho Echenim, Hervé Guiol, Nicolas Peltier
2018	J	`jnl`	On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic. CoRR Mnacho Echenim, Radu Iosif, Nicolas Peltier
2018	A*	`conf`	Prime Implicate Generation in Equational Logic (extended abstract). IJCAI Mnacho Echenim, Nicolas Peltier, Sophie Tourret
2018	A	`conf`	Superposition with Datatypes and Codatatypes. IJCAR Jasmin Christian Blanchette, Nicolas Peltier, Simon Robillard
2018	J	`jnl`	The Complexity of Prenex Separation Logic with One Selector. CoRR Mnacho Echenim, Radu Iosif, Nicolas Peltier
2017	J	`jnl`	A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules. J. Log. Comput. Nicolas Peltier
2017	J	`jnl`	CERES for first-order schemata. J. Log. Comput. Alexander Leitsch, Nicolas Peltier, Daniel Weller
2017	J	`jnl`	Prime Implicate Generation in Equational Logic. J. Artif. Intell. Res. Mnacho Echenim, Nicolas Peltier, Sophie Tourret
2017	A	`conf`	The Binomial Pricing Model in Finance: A Formalization in Isabelle. CADE Mnacho Echenim, Nicolas Peltier
2016	J	`jnl`	A Superposition Calculus for Abductive Reasoning. J. Autom. Reason. Mnacho Echenim, Nicolas Peltier
2016	J	`jnl`	A Variant of the Superposition Calculus. Arch. Formal Proofs Nicolas Peltier
2016	J	`jnl`	Proof Generalization in $$\mathrm {LK}$$ LK by Second Order Unifier Minimization. J. Autom. Reason. Thierry Boy de la Tour, Nicolas Peltier
2016	J	`jnl`	Propositional Resolution and Prime Implicates Generation. Arch. Formal Proofs Nicolas Peltier
2015	A	`conf`	A simulation framework for rapid prototyping and evaluation of thermal mitigation techniques in many-core architectures. ISLPED Tanguy Sassolas, Chiara Sandionigi, Alexandre Guerre, Julien Mottin, Pascal Vivet, Hela Boussetta, Nicolas Peltier
2015	A	`conf`	Quantifier-Free Equational Logic and Prime Implicate Generation. CADE Mnacho Echenim, Nicolas Peltier, Sophie Tourret
2015	C	`conf`	Reasoning on Schemas of Formulas: An Automata-Based Approach. LATA Nicolas Peltier
2014	J	`jnl`	A Complete Superposition Calculus for Primal Grammars. J. Autom. Reason. Hicham Bensaid, Nicolas Peltier
2014	—	`conf`	A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses. PAAR@IJCAR Sophie Tourret, Mnacho Echenim, Nicolas Peltier
2014	A	`conf`	A Rewriting Strategy to Generate Prime Implicates in Equational Logic. IJCAR Mnacho Echenim, Nicolas Peltier, Sophie Tourret
2014	J	`jnl`	A Superposition Calculus for Abductive Reasoning. CoRR Mnacho Echenim, Nicolas Peltier
2014	—	`ch.`	Analogy in Automated Deduction: A Survey. Computational Approaches to Analogical Reasoning Thierry Boy de la Tour, Nicolas Peltier
2014	J	`jnl`	Decidability and Undecidability Results for Propositional Schemata. CoRR Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
2014	A	`conf`	Early design stage thermal evaluation and mitigation: The locomotiv architectural case. DATE Tanguy Sassolas, Chiara Sandionigi, Alexandre Guerre, Alexandre Aminot, Pascal Vivet, Hela Boussetta, Luca Ferro, Nicolas Peltier
2014	—	`conf`	Thermal modeling methodology for efficient system-level thermal analysis. CICC Cristiano Santos, Pascal Vivet, Gene Matter, Nicolas Peltier, Sylvian Kaiser, Ricardo Augusto da Luz Reis
2014	J	`jnl`	Tractable and intractable classes of propositional schemata. J. Log. Comput. Nicolas Peltier
2013	J	`jnl`	A Resolution Calculus for First-order Schemata. Fundam. Informaticae Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier
2013	A*	`conf`	An Approach to Abductive Reasoning in Equational Logic. IJCAI Mnacho Echenim, Nicolas Peltier, Sophie Tourret
2013	—	`conf`	Combining Superposition and Induction: A Practical Realization. FroCos Abdelkader Kersani, Nicolas Peltier
2013	A	`conf`	Completeness and Decidability Results for First-Order Clauses with Indices. CADE Abdelkader Kersani, Nicolas Peltier
2013	J	`jnl`	Instantiation Schemes for Nested Theories. ACM Trans. Comput. Log. Mnacho Echenim, Nicolas Peltier
2013	B	`conf`	Schemata of Formulæ in the Theory of Arrays. TABLEAUX Nicolas Peltier
2013	—	`conf`	System-level thermal modeling for 3D circuits: Characterization with a 65nm memory-on-logic circuit. 3DIC Cristiano Santos, Pascal Vivet, Denis Dutoit, Philippe Garrault, Nicolas Peltier, Ricardo Reis
2012	J	`jnl`	A Calculus for Generating Ground Explanations (Technical Report) CoRR Mnacho Echenim, Nicolas Peltier
2012	A	`conf`	A Calculus for Generating Ground Explanations. IJCAR Mnacho Echenim, Nicolas Peltier
2012	J	`jnl`	An Instantiation Scheme for Satisfiability Modulo Theories. J. Autom. Reason. Mnacho Echenim, Nicolas Peltier
2012	J	`jnl`	First-order theorem proving: Foreword. J. Symb. Comput. Nicolas Peltier, Viorica Sofronie-Stokkermans
2012	J	`jnl`	Reasoning on Schemata of Formulae CoRR Mnacho Echenim, Nicolas Peltier
2012	—	`conf`	Reasoning on Schemata of Formulæ. AISC/MKM/Calculemus Mnacho Echenim, Nicolas Peltier
2011	J	`jnl`	Decidability and Undecidability Results for Propositional Schemata. J. Artif. Intell. Res. Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
2011	J	`jnl`	Generating Schemata of Resolution Proofs CoRR Vincent Aravantinos, Nicolas Peltier
2011	—	`conf`	Generating Schemata of Resolution Proofs. TABLEAUX (Workshops, Tutorials, and Short Papers) Vincent Aravantinos, Nicolas Peltier
2011	J	`jnl`	Instantiation Schemes for Nested Theories CoRR Mnacho Echenim, Nicolas Peltier
2011	J	`jnl`	Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version) CoRR Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
2011	C	`conf`	Linear Temporal Logic and Propositional Schemata, Back and Forth. TIME Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
2011	J	`jnl`	Modular instantiation schemes. Inf. Process. Lett. Mnacho Echenim, Nicolas Peltier
2011	B	`conf`	Schemata of SMT-Problems. TABLEAUX Vincent Aravantinos, Nicolas Peltier
2010	J	`jnl`	A Decidable Class of Nested Iterated Schemata (extended version) CoRR Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
2010	A	`conf`	A Decidable Class of Nested Iterated Schemata. IJCAR Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
2010	J	`jnl`	Bottom-up Construction of Semantic Tableaux. J. Log. Comput. Nicolas Peltier
2010	C	`conf`	Complexity of the Satisfiability Problem for a Class of Propositional Schemata. LATA Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
2010	—	`conf`	Instantiation of SMT Problems Modulo Integers. AISC/MKM/Calculemus Mnacho Echenim, Nicolas Peltier
2010	J	`jnl`	Instantiation of SMT problems modulo Integers CoRR Mnacho Echenim, Nicolas Peltier
2010	A	`conf`	Perfect Discrimination Graphs: Indexing Terms with Integer Exponents. IJCAR Hicham Bensaid, Ricardo Caferra, Nicolas Peltier
2010	—	`ed.`	Proceedings of the 7th International Workshop on First-Order Theorem Proving, FTP 2009, Oslo, Norway, July 6-7, 2009. FTP Nicolas Peltier, Viorica Sofronie-Stokkermans
2010	A	`conf`	RegSTAB: A SAT Solver for Propositional Schemata. IJCAR Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
2010	J	`jnl`	Simplified handling of iterated term schemata. Ann. Math. Artif. Intell. Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
2009	B	`conf`	A Schemata Calculus for Propositional Logic. TABLEAUX Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
2009	J	`jnl`	Constructing infinite models represented by tree automata. Ann. Math. Artif. Intell. Nicolas Peltier
2009	A	`conf`	Dei: A Theorem Prover for Terms with Integer Exponents. CADE Hicham Bensaid, Ricardo Caferra, Nicolas Peltier
2009	—	`conf`	Preface. FTP Nicolas Peltier, Viorica Sofronie-Stokkermans
2008	—	`conf`	A Needed Rewriting Strategy for Data-Structures with Pointers. RTA Rachid Echahed, Nicolas Peltier
2008	—	`conf`	A Unified View of Tree Automata and Term Schematisations. IFIP TCS Nicolas Peltier
2008	J	`jnl`	Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview. Int. J. Intell. Syst. Ricardo Caferra, Nicolas Peltier
2008	—	`conf`	Automated Model Building: From Finite to Infinite Models. AISC/MKM/Calculemus Nicolas Peltier
2008	J	`jnl`	Extended resolution simulates binary decision diagrams. Discret. Appl. Math. Nicolas Peltier
2008	Misc	`conf`	More Flexible Term Schematisations via Extended Primal Grammars. ISAIM Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier
2007	B	`conf`	A Bottom-Up Approach to Clausal Tableaux. TABLEAUX Nicolas Peltier
2007	J	`jnl`	A Resolution Calculus with Shared Literals. Fundam. Informaticae Nicolas Peltier
2007	—	`conf`	Non Strict Confluent Rewrite Systems for Data-Structures with Pointers. RTA Rachid Echahed, Nicolas Peltier
2007	C	`conf`	Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps. WoLLIC Hicham Bensaid, Ricardo Caferra, Nicolas Peltier
2006	B	`conf`	Narrowing Data-Structures with Pointers. ICGT Rachid Echahed, Nicolas Peltier
2006	C	`conf`	Rewriting term-graphs with priority. PPDP Ricardo Caferra, Rachid Echahed, Nicolas Peltier
2005	J	`jnl`	A Resolution Calculus for Shortening Proofs. Log. J. IGPL Nicolas Peltier
2005	J	`jnl`	Some Techniques for Proving Termination of the Hyperresolution Calculus. J. Autom. Reason. Nicolas Peltier
2004	J	`jnl`	A Proof Procedure for Functional First Order Logic Programs with Non-Deterministic Lazy Functions and Built-in Predicates. J. Funct. Log. Program. Nicolas Peltier
2004	J	`jnl`	Representing and Building Models for Decidable Subclasses of Equational Clausal Logic. J. Autom. Reason. Nicolas Peltier
2004	B	`conf`	Some Techniques for Branch-Saturation in Free-Variable Tableaux. JELIA Nicolas Peltier
2004	J	`jnl`	The first order theory of primal grammars is decidable. Theor. Comput. Sci. Nicolas Peltier
2003	B	`conf`	A More Efficient Tableaux Procedure for Simultaneous Search for Refutations and Finite Models. TABLEAUX Nicolas Peltier
2003	—	`conf`	A Resolution-based Model Building Algorithm for a Fragment of OCC1N=. FTP Nicolas Peltier
2003	J	`jnl`	A calculus combining resolution and enumeration for building finite models. J. Symb. Comput. Nicolas Peltier
2003	J	`jnl`	Building Infinite Models for Equational Clause Sets: Constructing Non-Ambiguous Formulae. Log. J. IGPL Nicolas Peltier
2003	J	`jnl`	Constructing Decision Procedures in Equational Clausal Logic. Fundam. Informaticae Nicolas Peltier
2003	J	`jnl`	Extracting models from clause sets saturated under semantic refinements of the resolution rule. Inf. Comput. Nicolas Peltier
2003	J	`jnl`	Model building with ordered resolution: extracting models from saturated clause sets. J. Symb. Comput. Nicolas Peltier
2001	A	`conf`	A General Method for Using Schematizations in Automated Deduction. IJCAR Nicolas Peltier
2001	J	`jnl`	On the decidability of the PVD class with equality. Log. J. IGPL Nicolas Peltier
2000	J	`jnl`	Combining Enumeration and Deductive Techniques in order to Increase the Class of Constructible Infinite Models. J. Symb. Comput. Ricardo Caferra, Nicolas Peltier
2000	—	`conf`	Emphasizing Human Techniques in Automated Geometry Theorem Proving: A Practical Realization. Automated Deduction in Geometry Ricardo Caferra, Nicolas Peltier, François Puitg
2000	—	`conf`	The Connection Method, Constraints and Model Building. Intellectics and Computational Logic Ricardo Caferra, Nicolas Peltier
2000	A	`conf`	Workshop: Model Computation - Principles, Algorithms, Applications. CADE Peter Baumgartner, Christian G. Fermüller, Nicolas Peltier, Hantao Zhang
1999	J	`jnl`	Pruning the Search Space and Extracting More Models in Tableaux. Log. J. IGPL Nicolas Peltier
1998	J	`jnl`	A New Method for Automated Finite Model Building Exploiting Failures and Symmetries. J. Log. Comput. Nicolas Peltier
1998	J	`jnl`	Semantic Generalizations for Proving and Disproving Conjectures by Analogy. J. Autom. Reason. Gilles Défourneaux, Christophe Bourely, Nicolas Peltier
1998	A	`conf`	System Description: An Equational Constraints Solver. CADE Nicolas Peltier
1997	J	`jnl`	A New Technique for Verifying and Correcting Logic Programs. J. Autom. Reason. Ricardo Caferra, Nicolas Peltier
1997	—	`conf`	Analogy and Abduction in Automated Deduction. IJCAI (1) Gilles Défourneaux, Nicolas Peltier
1997	J	`jnl`	Increasing Model Building Capabilities by Constraint Solving on Terms with Integer Exponents. J. Symb. Comput. Nicolas Peltier
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
1997	A	`conf`	Partial Matching for Analogy Discovery in Proofs and Counter-Examples. CADE Gilles Défourneaux, Nicolas Peltier
1997	B	`conf`	Simplifying and Generalizing Formulae in Tableaux. Pruning the Search Space and Building Models. TABLEAUX Nicolas Peltier
1997	J	`jnl`	Tree Automata and Automated Model Building. Fundam. Informaticae Nicolas Peltier
1996	—	`conf`	A Significant Extension of Logic Programming by Adapting Model Building Rules. ELP Ricardo Caferra, Nicolas Peltier
1996	B	`conf`	Building Proofs or Counterexamples by Analogy in a Resoluton Framework. JELIA Christophe Bourely, Gilles Défourneaux, Nicolas Peltier
1996	—	`conf`	Disc DISCO Christophe Bourely, Nicolas Peltier
1995	B	`conf`	Decision Procedures Using Model Building Techniques. CSL Ricardo Caferra, Nicolas Peltier
1995	A*	`conf`	Extending Semantic Resolution via Automated Model Building: Applications. IJCAI Ricardo Caferra, Nicolas Peltier
1995	B	`conf`	Model Building and Interactive Theory Discovery. TABLEAUX Ricardo Caferra, Nicolas Peltier
1994	A	`conf`	A Method for Building Models Automatically. Experiments with an Extension of OTTER. CADE Christophe Bourely, Ricardo Caferra, Nicolas Peltier