Ban3

Informations sur l'auteur

Nicolas Peltier

http://membres-lig.imag.fr/peltier/

http://pistou.imag.fr/site/author/316

  
Équipe(s) :
CAPP Du 01/01/2007 au 31/12/2099 		 

Publications de l'auteur

La liste contient 96 élément(s)

(Les éditeurs apparaissent en italique)


Ajouter toute la liste au panier

Exporter la liste au format
Retrier la liste par :

International peer reviewed journal [ACL]
2012
1
Mnacho Echenim, Nicolas Peltier.
An Instantiation Scheme for Satisfiability Modulo Theories.
Journal of Automated Reasoning, 2012.
Www-128x128
bibtex/ html
2011
2
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier.
Decidability and Undecidability Results for Propositional Schemata.
Journal of Artificial Intelligence Research, 40:599--656, 2011.
Www-128x128
bibtex/ html
3
Mnacho Echenim, Nicolas Peltier.
Modular instantiation schemes.
Information Processing Letters, 2011.
bibtex/ html
2010
4
Nicolas Peltier.
Bottom-up Construction of Semantic Tableaux.
Journal of Logic and Computation, 20(1), 2010.
bibtex/ html
5
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier.
Simplified Handling of Iterated Term Schemata.
Annals of Mathematics and Artificial Intelligence, 2010. Note: Accepted, to appear.
bibtex/ html
2009
6
Nicolas Peltier.
Constructing Infinite Models Represented By Tree Automata.
Annals of Mathematics and Artificial Intelligence, 56(1):65, 2009.
bibtex/ html
2008
7
Ricardo Caferra, Rachid Echahed, Nicolas Peltier.
A Term-Graph Clausal Logic: Completeness and Incompleteness Results.
Journal of Applied Non-Classical Logics, 18(4):373--411, 2008.
bibtex/ html
8
Ricardo Caferra, Nicolas Peltier.
Accepting/Rejecting Propositions from Accepted/Rejected Propositions: a Unifying Overview.
International Journal of Intelligent Systems, 23(10):999-1020, 2008.
bibtex/ html
9
Nicolas Peltier.
Extended Resolution Simulates Binary Decision Diagrams.
Discrete Applied Mathematics, 156:825--837, 2008.
bibtex/ html
2007
10
Nicolas Peltier.
A Resolution Calculus with Shared Literals.
Fundamenta Informaticae, 76(4):449--480, 2007.
bibtex/ html
2006
11
Nicolas Peltier.
Some Techniques for Proving Termination of the Hyperresolution Calculus.
Journal of Automated Reasoning, 35:391--427, 2006.
bibtex/ html
2005
12
Nicolas Peltier.
Representing and Building Models for Decidable Subclasses of Equational Clausal Logic.
Journal of Automated Reasoning, 33(2):133--170, 2005.
bibtex/ html
13
Nicolas Peltier.
A Resolution Calculus for Shortening Proofs.
Logic Journal of the Interest Group in Pure and Applied Logics, 13:307--333, 2005.
bibtex/ html
2004
14
Nicolas Peltier.
The First Order Theory of Primal Grammars is Decidable.
Theoretical Computer Science, 323:267--320, 2004.
bibtex/ html
15
Nicolas Peltier.
A Proof Procedure for Functional First Order Logic Programs with Non-Deterministic Lazy Functions and Built-in Predicates.
Journal of Functional and Logic Programming, 2004(3), nov 2004.
bibtex/ html
2003
16
Nicolas Peltier.
A Calculus Combining Resolution and Enumeration for Building Finite Models.
Journal of Symbolic Computation, 36(1-2):49--77, 2003.
bibtex/ html
17
Nicolas Peltier.
Model Building with Ordered Resolution: extracting models from saturated clause sets.
Journal of Symbolic Computation, 36(1-2):5--48, 2003.
bibtex/ html
18
Nicolas Peltier.
Extracting Models from Clause Sets Saturated under Semantic Refinements of the Resolution Rule.
Information and Computation, 181:99-130, 2003.
bibtex/ html
19
Nicolas Peltier.
Building Infinite Models for Equational Clause Sets: Constructing Non-Ambiguous Formulae.
Logic Journal of the IGPL, 11(1):103--137, 2003.
bibtex/ html
20
Nicolas Peltier.
Constructing decision procedures in equational clausal logic.
Fundamenta Informaticae, 54(1):17--65, 2003.
bibtex/ html
2001
21
Nicolas Peltier.
On the decidability of the PVD class with equality.
Logic Journal of the IGPL, 9(4):601--624, 2001.
bibtex/ html
2000
22
Ricardo Caferra, Nicolas Peltier.
Combining Enumeration and Deductive Techniques in order to Increase the Class of Constructible Infinite Models.
Journal of Symbolic Computation, 29:177--211, 2000.
bibtex/ html
1999
23
Nicolas Peltier.
Pruning the Search Space and Extracting More Models in Tableaux.
Logic Journal of the IGPL, 7(2):217--251, 1999.
bibtex/ html
1998
24
G. Défourneaux, Ch. Bourely, Nicolas Peltier.
Semantic Generalizations for Proving and Disproving conjectures by Analogy.
Journal of Automated Reasoning, 20(1 & 2):27--45, 1998.
bibtex/ html
25
Nicolas Peltier.
A new method for automated finite model building exploiting failures and symmetries.
Journal of Logic and Computation, 8(4):511--543, 1998.
bibtex/ html
1997
26
Ricardo Caferra, Nicolas Peltier.
A new technique for verifying and correcting logic programs.
Journal of Automated Reasoning, 19(3):277--318, 1997.
bibtex/ html
27
Nicolas Peltier.
Increasing the capabilities of Model building by constraint solving with terms with integer exponents.
Journal of Symbolic Computation, 24:59-101, 1997.
bibtex/ html
28
Nicolas Peltier.
Tree Automata and Automated Model Building.
Fundamenta Informaticae, 30(1):59--81, 1997.
bibtex/ html
International peer-reviewed conference proceedings [ACT]
2012
29
Mnacho Echenim, Nicolas Peltier.
A Calculus for Generating Ground Explanations.
Proceedings of the International Joint Conference on Automated Reasoning (IJCAR'12), 2012.
bibtex/ html
30
Mnacho Echenim, Nicolas Peltier.
Reasoning on Schemata of Formulae.
Proceedings of CICM 2012 (Conferences on Intelligent Computer Mathematics), 2012.
bibtex/ html
2011
31
Vincent Aravantinos, Nicolas Peltier.
Schemata of SMT problems.
TABLEAUX 11 (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), LNCS, 2011.
bibtex/ html
32
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier.
Linear Temporal Logic and Propositional Schemata, Back and Forth.
TIME'2011 - 18th International Symposium on Temporal Representation and Reasoning, 2011.
bibtex/ html
33
Vincent Aravantinos, Nicolas Peltier.
Generating Schemata of Resolution Proofs.
FTP-2011 (International Workshop on First-Order Theorem Proving), 2011.
bibtex/ html
2010
34
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier.
Complexity of the Satisfiability Problem for a Class of Propositional Schemata.
LATA 2010 (Language, Automata Theory and Applications), LNCS, 2010.
bibtex/ html
35
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier.
A Decidable Class of Nested Iterated Schemata.
IJCAR 2010 (International Joint Conference on Automated Reasoning), LNCS, 2010.
bibtex/ html
36
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier.
RegSTAB: a SAT-Solver for Propositional Schemata.
IJCAR 2010 (International Joint Conference on Automated Reasoning), LNCS, 2010.
bibtex/ html
37
Hicham Bensaid, Ricardo Caferra, Nicolas Peltier.
Perfect discrimination graphs: indexing terms with integer exponents.
IJCAR 2010 (International Joint Conference on Automated Reasoning), LNCS, 2010.
bibtex/ html
38
Mnacho Echenim, Nicolas Peltier.
Instantiation of SMT problems modulo Integers.
AISC 2010 (10th International Conference on Artificial Intelligence and Symbolic Computation), LNCS, 2010.
bibtex/ html
39
Hicham Bensaid, Ricardo Caferra, Nicolas Peltier.
I-terms in ordered resolution and superposition calculi : retrieving lost completeness.
AISC 2010 (10th International Conference on Artificial Intelligence and Symbolic Computation), LNCS, 2010.
bibtex/ html
2009
40
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier.
A Schemata Calculus For Propositional Logic.
TABLEAUX 09 (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), 5607:32-46, LNCS, 2009.
bibtex/ html
41
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier.
A DPLL Proof Procedure for Propositional Iterated Schemata.
Workshop ``Structures and Deduction 2009'' (ESSLI), :24--38, 2009.
bibtex/ html
42
Hicham Bensaid, Ricardo Caferra, Nicolas Peltier.
DEI: A Theorem Prover for Terms with Integer Exponents.
CADE 22 (22nd International Conference on Automated Deduction), 5663:146--150, Lecture Notes in Computer Science, 2009.
bibtex/ html
2008
43
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier.
More Flexible Term Schematisations via Extended Primal Grammars.
Tenth International Symposium on Artificial Intelligence and Mathematics (ISAIM), jan 2008.
bibtex/ html
44
Rachid Echahed, Nicolas Peltier.
A Needed Rewriting Strategy for Data-Structures with Pointers.
Rewriting Techniques and Applications, 19th International Conference, RTA 2008, 5117:63-78, Lecture Notes in Computer Science, 2008.
bibtex/ html
45
Nicolas Peltier.
A Unified View of Tree Automata and Term Schematisations.
Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, 273:491-505, IFIP, 2008.
bibtex/ html
46
Nicolas Peltier.
Automated Model Building: From Finite to Infinite Models.
9th International Conference on Artificial Intelligence and Symbolic Computation, 5144:155-169, 2008.
bibtex/ html
2007
47
Rachid Echahed, Nicolas Peltier.
Non Strict Confluent Rewrite Systems for Data-Structures with Pointers.
Proceedings of RTA (Rewriting Techniques and Applications), jun 2007.
bibtex/ html
48
Nicolas Peltier.
A Bottom-up Approach to Clausal Tableaux.
TABLEAUX'07 (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), jul 2007. Note: Aix en Provence, France..
bibtex/ html
49
Hicham Bensaid, Ricardo Caferra, Nicolas Peltier.
Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps.
Proc. Wollic'07 (Workshop on Logic, Language, Information and Computation), :38--52, jul 2007. Note: LNCS 4576.
bibtex/ html
2006
50
Ricardo Caferra, Rachid Echahed, Nicolas Peltier.
Rewriting Term-Graphs with Priority.
Proceedings of the Eighth ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, :109--120, 2006.
bibtex/ html
51
Rachid Echahed, Nicolas Peltier.
Narrowing Data-Structures with Pointers.
Proceedings of ICGT (International Conference of Graph Transformation), sep 2006.
bibtex/ html
2005
52
Ricardo Caferra, Rachid Echahed, Nicolas Peltier.
R. Letz.
A Graph Clausal Logic.
FTP'05 (International Workshop First-Order Theorem Proving)., :85--96, sep 2005. Note: Koblenz, Germany.
bibtex/ html
2004
53
Nicolas Peltier.
J. Alferes, J. Leite.
Some Techniques for Branch-Saturation in Free-Variable Tableaux.
JELIA'04 (Logics in Artificial Intelligence, Ninth European Conference), sep 2004.
bibtex/ html
2003
54
Nicolas Peltier.
Ingo Dahn, Laurent Vigneron.
A Resolution-based Model Building Algorithm for a Fragment of OCC1N=.
Electronic Notes in Theoretical Computer Science, 86, 2003.
bibtex/ html
55
Nicolas Peltier.
Ingo Dahn, Laurent Vigneron.
A Resolution-based Model Building Algorithm for a Fragment of $cal OCC}1cal N}_=$.
FTP'03 (Fourth International Workshop First-Order Theorem Proving), jun 2003.
bibtex/ html
56
Nicolas Peltier.
A more efficient tableau procedure for simultaneous search for refutations and finite models.
TABLEAUX'03 (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), sep 2003. Note: Roma, Italy.
bibtex/ html
2001
57
Nicolas Peltier.
A General Method for Using Terms Schematizations in Automated Deduction.
Proceedings of the International Joint Conference on Automated Reasoning (IJCAR'01), :578--593, 2001.
bibtex/ html
2000
58
Ricardo Caferra, Nicolas Peltier.
The Connection Method, Constraints and Model Building.
Intellectics and Computational Logic, 19:67--84, Applied Logic Series, 2000.
bibtex/ html
59
Ricardo Caferra, Nicolas Peltier, François Puitg.
J. Richter-Gebert, Dongming Wang.
Emphazing human techniques in geometry automated theorem proving:a practical realization.
Workshop on Automated Deduction in Geometry. Zurich, Switzlerland, sep 2000.
bibtex/ html
60
Nicolas Peltier.
Peter Baumgartner, Haihong Zhang.
Combining Resolution and Enumeration for Finite Model Building.
FTP'00 (Third International Workshop First-Order Theorem Proving), :170--181, jul 2000. Note: St-Andrews, Scotland.
bibtex/ html
61
Nicolas Peltier.
Peter Baumgartner, Haihong Zhang.
Model Building with Ordered Resolution.
FTP'00 (Third International Workshop First-Order Theorem Proving)., :158--169, jul 2000. Note: St-Andrews, Scotland.
bibtex/ html
1998
62
Nicolas Peltier.
An equational constraints solver.
Proceedings of CADE-15, :119-123, 1998.
bibtex/ html
1997
63
G. Défourneaux, Nicolas Peltier.
William McCune.
Partial Matching for Analogy Discovery in Proofs and Counter-examples.
Proceedings of CADE 14, jul 1997.
bibtex/ html
64
G. Défourneaux, Nicolas Peltier.
M. E. Pollack.
Analogy and Abduction in Automated Reasoning.
Proceedings of IJCAI'97, Nagoya, Japan, aug 1997.
bibtex/ html
65
Nicolas Peltier.
Simplifying formulae in Tableaux. Pruning the search space and building models.
Proceeding of Tableaux'97, :313--327, 1997.
bibtex/ html
1996
66
Ch. Bourely, G. Défourneaux, Nicolas Peltier.
Building Proofs or Counterexamples by Analogy in a Resolution Framework.
Proceedings of JELIA 96, :34--49, 1996.
bibtex/ html
67
Ch. Bourely, Nicolas Peltier.
DISC-ATINF: a System for Implementing Strategies and Calculi.
Proceeding of DISCO'96, 1996.
bibtex/ html
68
Ricardo Caferra, Nicolas Peltier.
A significant extension of logic programming by adapting model buildings rules.
Proc. of Extensions of Logic Programming 96, :51--65, mar 1996.
bibtex/ html
69
Ricardo Caferra, Nicolas Peltier.
Decision Procedures using Model Building techniques.
Proceeding of Computer Science Logic, CSL'95, :130--144, 1996.
bibtex/ html
1995
70
Ricardo Caferra, Nicolas Peltier.
Model Building and Interactive Theory Discovery.
Proceeding of Tableaux'95, :154--168, LNAI 918, 1995.
bibtex/ html
71
Ricardo Caferra, Nicolas Peltier.
Extending semantic resolution via automated model building: applications.
Proceeding of IJCAI'95, :328--334, 1995.
bibtex/ html
Scientific books and chapter [OS]
2004
72
Ricardo Caferra, A. Leitsch, Nicolas Peltier.
Automated Model Building.
31, Applied Logic Series, Kluwer Academic Publishers, 2004.
bibtex/ html
1998
73
Ricardo Caferra, Nicolas Peltier.
Disinference rules, model building and abduction.
``Logic at work. Essays dedicated to the memory of Helena Rasiowa'' (Part 5:Logic in Computer Science, Chap. 20), 20, :331--353, Physica-Verlag, 1998.
bibtex/ html
Book or Proceedings editing [DO]
2000
74
Peter Baumgartner, Chris Fermüller, Nicolas Peltier, Hantao Zhang.
CADE-17 Workshop on Model Computation - Principles, Algorithms, Applications.
2000.
bibtex/ html
Doctoral Dissertations and Habilitations Theses [TH]
2007
75
Nicolas Peltier.
Contributions à une approche qualitative de la déduction automatique.
Habilitation à Diriger des Recherches, Grenoble INP, jun 2007.
bibtex/ html
1997
76
Nicolas Peltier.
Nouvelles Techniques pour la Construction de Modèles finis ou infinis en Déduction Automatique.
PhD Thesis, Institut National Polytechnique de Grenoble, 1997.
bibtex/ html
Other Publications [AP]
2012
77
Mnacho Echenim, Nicolas Peltier.
A Calculus for Generating Ground Explanations (Technical Report).
CoRR, abs/1201.5954, 2012.
Www-128x128
bibtex/ html
2011
78
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier.
Linear Temporal Logic and Propositional Schemata, Back and Forth (extended version).
Technical Report, abs/1102.2174, 2011.
bibtex/ html
79
Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier.
A Resolution Calculus for Propositional Schemata.
Research Report, 2011.
Pdf-128x128
bibtex/ html
80
Vincent Aravantinos, Mnacho Echenim, Nicolas Peltier.
A Resolution Calculus for First-Order Schemata.
Technical Report, 2011.
bibtex/ html
2010
81
Rachid Echahed, Nicolas Peltier.
Priority-Independent Rewrite Systems for Pointer-based Data-Structures.
Technical Report, Technical report, University of Grenoble., 2010.
Pdf-128x128
bibtex/ html
82
Mnacho Echenim, Nicolas Peltier.
Instantiation of SMT problems modulo Integers (technical report).
Technical Report, University of Grenoble, 2010.
Www-128x128
bibtex/ html
83
Vincent Aravantinos, Ricardo Caferra, Nicolas Peltier.
A Decidable Class of Nested Iterated Schemata (extended version).
Technical Report, University of Grenoble, 2010.
Www-128x128
bibtex/ html
2003
84
Nicolas Balacheff, Ricardo Caferra, Nicolas Peltier, Sylvie Pesty, Sophie Soury-Lavergne, Rosamund Sutherland, Jana Trgalova, Carine Webber, Michelle Cerulli, Nathalie Gaudin, Mirko Marraci, M.A. Mariotti, Jean-Michel Muller, Jean-François Nicaud, Michel Occello, Federica Olivero.
Baghera Assessment Project, designing an hybrid and emergent educational society.
Technical Report, 2003. Note: Edited by Sophie Soury-Lavergne ; Available at: http://www-leibniz.imag.fr/LesCahiers/2003/Cahier81/{BAP}_CahiersLaboLeibniz.{PDF} Research report {IST}-2001-33046.
Www-128x128 [ abstract ]
bibtex/ html
85
Ricardo Caferra, Nicolas Peltier.
HOARD-ATINF - A generic logical theorem prover.
Published in the report of the Baghera European Project BAP: ``Designing an hybrid and emergent educational society'', jan 2003.
bibtex/ html
2002
86
Nicolas Peltier.
HOARD-ATINF. A Logical Theorem Prover for Teaching Proof in Geometry..
ACA'02, Application of Computer Algebra, Volos, Greece., 2002.
bibtex/ html
2001
87
Nicolas Peltier.
Using Term Schematizations in Automated Deduction.
Research Report. Available on {\tt http://membres-lig.imag.fr/ATINF/Nicolas.Peltier/}, 2001.
bibtex/ html
88
Nicolas Peltier.
HOARD-ATINF - Manuel d'utilisation.
Research Report. Available on {\tt http://membres-lig.imag.fr/ATINF/Nicolas.Peltier/}, 2001.
bibtex/ html
89
Nicolas Peltier.
Introduction à la Déduction Automatique.
Note du cours ``Logique et Formalisation du raisonnement (partie II: introduction à la déduction automatique).'', DEA ISC. Université Joseph Fourier, Grenoble., 2001.
bibtex/ html
1999
90
Nicolas Peltier.
Searching for Clauses Sets with only one Herbrand Model.
Workshop on Model Building. Grenoble., sep 1999. Note: Published in the {\em Cahiers du Laboratoire Leibniz} (No 15, Nov. 00).
bibtex/ html
1998
91
Nicolas Peltier.
Can model builders help logicians in building infinite models ?.
AAR Newsletter, 1998.
bibtex/ html
92
Nicolas Peltier.
Proof Generalization and Function Introduction.
FTP'98 (International Workshop First-Order Theorem Proving)., 1998.
bibtex/ html
1997
93
Ricardo Caferra, Nicolas Peltier.
Combining inference and disinference rules with enumeration for model building.
Workshop on model-based reasoning. IJCAI'97, 1997.
bibtex/ html
94
Ricardo Caferra, Nicolas Peltier.
Model building in the cross-roads of consequence and non-consequence relations.
FTP'97 (International Workshop First-Order Theorem Proving). Technical Report RISC-Linz Report Series No. 97-50, page 40-44., 1997.
bibtex/ html
95
Stéphane Fèvre, Nicolas Peltier.
Two problems in geometry solved by using automated model builders.
AAR Newsletter 38, 1997.
bibtex/ html
1994
96
Nicolas Peltier.
Construction de Modèles en Déduction Automatique.
Mémoire de DEA, Juin 1994.
bibtex/ html