Centre de diffusion de revues académiques mathématiques

 
 
 
 

Les cours du CIRM

Table des matières de ce fascicule | Article précédent | Article suivant
Loïc Pottier
Preuves formelles automatiques et calcul formel
Les cours du CIRM, 2 no. 1: Journées Nationales de Calcul Formel (2011), Exp. No. 3, 25 p., doi: 10.5802/ccirm.15
Article PDF

Bibliographie

[1] Stuart F. Allen, Robert L. Constable, Douglas J. Howe & William E. Aitken, The Semantics of Reflected Proof, LICS, IEEE Computer Society, 1990, p. 95-105  MR 1099164
[2] Samuel Boutin, “Réflexions sur les quotients.”, Thèse d’informatique, Université Paris VII (1997)
[3] Bruno Buchberger, “Bruno Buchberger’s PhD thesis 1965 : An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal”, Journal of Symbolic Computation 41 (2006) no. 3-4  MR 2202562 |  Zbl 1158.01307
[4] Amine Chaieb & Makarius Wenzel, Context Aware Calculation and Deduction., Calculemus/MKM, Springer-Verlag, 2007, p. 27-39
[5] Bruce W. Char, Gregory J. Fee, Keith O. Geddes, Gaston H. Gonnet & Michael B. Monagan, “A Tutorial Introduction to MAPLE”, Journal of Symbolic Computation 2 (1986) no. 2, p. 179-200
[6] Shang-Ching Chou, Mechanical geometry theorem proving, Kluwer Academic Publishers, 1987  MR 998773
[7] David Eisenbud, Commutative Algebra : with a View Toward Algebraic Geometry, Graduate Texts in Mathematics, Springer-Verlag, 1999  MR 1322960 |  Zbl 0819.13001
[8] Marc Giusti, Joos Heintz, Jose Enrique Morais, Jacques Morgenstern & Luis Miguel Pardo, “Straight-line programs in geometric elimination theory”, Journal of Pure and Applied Algebra 124 (1998) no. 1/3, p. 101-146  Zbl 0944.12004
[9] Daniel R. Grayson & Michael E. Stillman, “Macaulay2”, http://www.math.uiuc.edu/Macaulay2/
[10] Benjamin Grégoire & Xavier Leroy, A compiled implementation of strong reduction, International Conference on Functional Programming 2002, ACM Press, 2002, p. 235-246
[11] Benjamin Grégoire & Assia Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq, TPHOLs 2005, Springer-Verlag, 2005, p. 98-113  MR 2197007 |  Zbl 1152.68702
[12] Benjamin Grégoire, Loïc Pottier & Laurent Théry, “Proof Certificates for Algebra and their Application to Automatic Geometry Theorem Proving”, Automated Deduction in Geometry, ADG 2008, Revised Papers, Lecture Notes in Computer Science 6301 (2011) no. 2  Zbl pre05899968
[13] Benjamin Grégoire, Laurent Théry & Benjamin Werner, A computational approach to Pocklington certificates in type theory, FLOPS’06, Springer-Verlag, 2006, p. 97-113  Zbl 1185.68621
[14] John Harrison, HOL Light : A tutorial introduction, FMCAD’96, Springer-Verlag, 1996, p. 265–269
[15] John Harrison, Complex quantifier elimination in HOL, in TPHOLs 2001 : Supplemental Proceedings, Division of Informatics, University of Edinburgh, Published as Informatics Report Series EDI-INF-RR-0046, 2001, p. 159-174
[16] John Harrison, Automating elementary number-theoretic proofs using Gröbner bases, CADE 21, Springer-Verlag, 2007, p. 51–66  MR 2458072 |  Zbl 1213.03020
[17] John Harrison, Verifying nonlinear real formulas via sums of squares, TPHOLs’2007, Springer-Verlag, 2007, p. 102–118  MR 2550881 |  Zbl 1144.68357
[18] John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009  MR 2503047 |  Zbl 1178.03001
[19] Deepak Kapur, Geometry theorem proving using Hilbert’s Nullstellensatz, SYMSAC ’86 : Proceedings of the fifth ACM symposium on Symbolic and algebraic computation, ACM, 1986, p. 202–208
[20] Deepak Kapur, “A refutational approach to geometry theorem proving”, Artificial Intelligence 37 (1988) no. 1-3, p. 61-93  MR 987644 |  Zbl 0678.68094
[21] Deepak Kapur, Automated Geometric Reasoning : Dixon Resultants, Gröbner Bases, and Characteristic Sets, Automated Deduction in Geometry, Springer-Verlag, 1996, p. 1-36  Zbl 0910.03010
[22] Lawrence C. Paulson, “Isabelle : A generic theorem prover”, Journal of Automated Reasoning 828 (1994)  MR 1313213 |  Zbl 0825.68059
[23] Loïc Pottier, Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics, in Proceedings of the LPAR Workshops : Knowledge Exchange : Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics, CEUR Workshop Proceedings, 2008
[24] Judit Robu, Geometry Theorem Proving in the Frame of the Theorema Project, Technical report 02-23, RISC Report Series, University of Linz, Austria, 2002
[25] Laurent Théry, “A Machine-Checked Implementation of Buchberger’s Algorithm”, Journal of Automated Reasoning 26 (2001) no. 2  MR 1812745 |  Zbl 0964.03012
[26] Freek Wiedijk, Formalizing 100 Theorems, http://www.cs.ru.nl/~freek/100
[27] Wen-Tsun Wu, On the Decision Problem and the Mechanization of Theorem-Proving in Elementary Geometry, Automated Theorem Proving - After 25 Years, American Mathematical Society, 1984, p. 213-234  MR 749248 |  Zbl 0578.68078
Copyright Cellule MathDoc 2014 | Crédit | Plan du site