Centre de diffusion de revues académiques mathématiques
Accueil
Les cours du CIRM
Table des matières de ce fascicule | Article précédent | Article suivantLoï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
[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