Preuves formelles automatiques et calcul formel

Pottier, Loïc

Journées Nationales de Calcul Formel. 14 – 18 Novembre 2011, Les cours du CIRM, no. 1 (2011), Exposé no. 3, 25 p.

[1] Allen, Stuart F.; Constable, Robert L.; Howe, Douglas J.; Aitken, William E. The Semantics of Reflected Proof, LICS, IEEE Computer Society, 1990, pp. 95-105

[2] Boutin, Samuel Réflexions sur les quotients., Thèse d’informatique, Université Paris VII (1997)

[3] Buchberger, Bruno 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, Volume 41 (2006) no. 3-4

[4] Chaieb, Amine; Wenzel, Makarius Context Aware Calculation and Deduction., Calculemus/MKM (LNCS), Volume 4573, Springer-Verlag, 2007, pp. 27-39

[5] Char, Bruce W.; Fee, Gregory J.; Geddes, Keith O.; Gonnet, Gaston H.; Monagan, Michael B. A Tutorial Introduction to MAPLE, Journal of Symbolic Computation, Volume 2 (1986) no. 2, pp. 179-200

[6] Chou, Shang-Ching Mechanical geometry theorem proving, Kluwer Academic Publishers, 1987

[7] Eisenbud, David Commutative Algebra : with a View Toward Algebraic Geometry, Graduate Texts in Mathematics, Springer-Verlag, 1999

[8] Giusti, Marc; Heintz, Joos; Morais, Jose Enrique; Morgenstern, Jacques; Pardo, Luis Miguel Straight-line programs in geometric elimination theory, Journal of Pure and Applied Algebra, Volume 124 (1998) no. 1/3, pp. 101-146

[9] Grayson, Daniel R.; Stillman, Michael E. Macaulay2 (http://www.math.uiuc.edu/Macaulay2/)

[10] Grégoire, Benjamin; Leroy, Xavier A compiled implementation of strong reduction, International Conference on Functional Programming 2002, ACM Press, 2002, pp. 235-246

[11] Grégoire, Benjamin; Mahboubi, Assia Proving Equalities in a Commutative Ring Done Right in Coq, TPHOLs 2005 (LNCS), Volume 3603, Springer-Verlag, 2005, pp. 98-113

[12] Grégoire, Benjamin; Pottier, Loïc; Théry, Laurent 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, Volume 6301 (2011) no. 2

[13] Grégoire, Benjamin; Théry, Laurent; Werner, Benjamin A computational approach to Pocklington certificates in type theory, FLOPS’06 (LNCS), Volume 3945, Springer-Verlag, 2006, pp. 97-113

[14] Harrison, John HOL Light : A tutorial introduction, FMCAD’96 (LNCS), Volume 1166, Springer-Verlag, 1996, pp. 265-269

[15] Harrison, John Complex quantifier elimination in HOL, TPHOLs 2001 : Supplemental Proceedings, Division of Informatics, University of Edinburgh (2001), pp. 159-174 (Published as Informatics Report Series EDI-INF-RR-0046)

[16] Harrison, John Automating elementary number-theoretic proofs using Gröbner bases, CADE 21 (LNCS), Volume 4603, Springer-Verlag, 2007, pp. 51-66

[17] Harrison, John Verifying nonlinear real formulas via sums of squares, TPHOLs’2007 (LNCS), Volume 4732, Springer-Verlag, 2007, pp. 102-118

[18] Harrison, John Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009

[19] Kapur, Deepak Geometry theorem proving using Hilbert’s Nullstellensatz, SYMSAC ’86 : Proceedings of the fifth ACM symposium on Symbolic and algebraic computation, ACM, 1986, pp. 202-208

[20] Kapur, Deepak A refutational approach to geometry theorem proving, Artificial Intelligence, Volume 37 (1988) no. 1-3, pp. 61-93

[21] Kapur, Deepak Automated Geometric Reasoning : Dixon Resultants, Gröbner Bases, and Characteristic Sets, Automated Deduction in Geometry (LNCS), Volume 1360, Springer-Verlag, 1996, pp. 1-36

[22] Paulson, Lawrence C. Isabelle : A generic theorem prover, Journal of Automated Reasoning, Volume 828 (1994)

[23] Pottier, Loïc Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics, 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) no. 418

[24] Robu, Judit Geometry Theorem Proving in the Frame of the Theorema Project (2002) no. 02-23 (Technical report PhD Thesis)

[25] Théry, Laurent A Machine-Checked Implementation of Buchberger’s Algorithm, Journal of Automated Reasoning, Volume 26 (2001) no. 2

[26] Wiedijk, Freek Formalizing 100 Theorems (http://www.cs.ru.nl/~freek/100)

[27] Wu, Wen-Tsun On the Decision Problem and the Mechanization of Theorem-Proving in Elementary Geometry, Automated Theorem Proving - After 25 Years, American Mathematical Society, 1984, pp. 213-234