Mersenne banner
no. 1
Preuves formelles automatiques et calcul formel
Loïc Pottier1
1 Equipe-projet Marelle, INRIA Sophia Antipolis
Les cours du CIRM, Tome 2 (2011) no. 1, Exposé no. 3, 25 p.
Publié le :
DOI : 10.5802/ccirm.15
Loïc Pottier 1

1 Equipe-projet Marelle, INRIA Sophia Antipolis 
@article{CCIRM_2011__2_1_A3_0,
     author = {Lo{\"\i}c Pottier},
     title = {Preuves formelles automatiques et calcul formel},
     journal = {Les cours du CIRM},
     note = {talk:3},
     publisher = {CIRM},
     volume = {2},
     number = {1},
     year = {2011},
     doi = {10.5802/ccirm.15},
     language = {fr},
     url = {https://ccirm.centre-mersenne.org/articles/10.5802/ccirm.15/}
}
TY  - JOUR
AU  - Loïc Pottier
TI  - Preuves formelles automatiques et calcul formel
JO  - Les cours du CIRM
N1  - talk:3
PY  - 2011
VL  - 2
IS  - 1
PB  - CIRM
UR  - https://ccirm.centre-mersenne.org/articles/10.5802/ccirm.15/
DO  - 10.5802/ccirm.15
LA  - fr
ID  - CCIRM_2011__2_1_A3_0
ER  - 
%0 Journal Article
%A Loïc Pottier
%T Preuves formelles automatiques et calcul formel
%J Les cours du CIRM
%Z talk:3
%D 2011
%V 2
%N 1
%I CIRM
%U https://ccirm.centre-mersenne.org/articles/10.5802/ccirm.15/
%R 10.5802/ccirm.15
%G fr
%F CCIRM_2011__2_1_A3_0
Loïc Pottier. Preuves formelles automatiques et calcul formel. Les cours du CIRM, Tome 2 (2011) no. 1, Exposé no. 3, 25 p. doi : 10.5802/ccirm.15. https://ccirm.centre-mersenne.org/articles/10.5802/ccirm.15/

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

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

[4] Amine Chaieb; Makarius Wenzel Context Aware Calculation and Deduction., Calculemus/MKM (LNCS), Volume 4573, Springer-Verlag, 2007, pp. 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, Volume 2 (1986) no. 2, pp. 179-200

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

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

[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, Volume 124 (1998) no. 1/3, pp. 101-146

[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, pp. 235-246

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

[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, Volume 6301 (2011) no. 2

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

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

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

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

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

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

[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, pp. 202-208

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

[21] Deepak Kapur 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] Lawrence C. Paulson Isabelle : A generic theorem prover, Journal of Automated Reasoning, Volume 828 (1994)

[23] Loïc Pottier 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 (2008) no. 418

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

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

[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, pp. 213-234

Cité par Sources :