Preuves formelles automatiques et calcul formel

 Access to full text

 Full (PDF)

1. Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William E. Aitken, The Semantics of Reflected Proof, LICS (1990), 95-105, IEEE Computer Society MR1099164
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) Zbl1158.01307MR2202562
4. Amine Chaieb, Makarius Wenzel, Context Aware Calculation and Deduction., Calculemus/MKM 4573 (2007), 27-39, Springer-Verlag Zbl1202.68375
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), 179-200 
6. Shang-Ching Chou, Mechanical geometry theorem proving, (1987), Kluwer Academic Publishers Zbl0661.14037MR998773
7. David Eisenbud, Commutative Algebra : with a View Toward Algebraic Geometry, (1999), Springer-Verlag Zbl0819.13001MR1322960
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), 101-146 Zbl0944.12004
9. Daniel R. Grayson, Michael E. Stillman, Macaulay2 
10. Benjamin Grégoire, Xavier Leroy, A compiled implementation of strong reduction, International Conference on Functional Programming 2002 (2002), 235-246, ACM Press Zbl1322.68053
11. Benjamin Grégoire, Assia Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq, TPHOLs 2005 3603 (2005), 98-113, Springer-Verlag Zbl1152.68702MR2197007
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) Zbl1302.68242
13. Benjamin Grégoire, Laurent Théry, Benjamin Werner, A computational approach to Pocklington certificates in type theory, FLOPS’06 3945 (2006), 97-113, Springer-Verlag Zbl1185.68621
14. John Harrison, HOL Light : A tutorial introduction, FMCAD’96 1166 (1996), 265-269, Springer-Verlag 
15. John Harrison, Complex quantifier elimination in HOL, TPHOLs 2001 : Supplemental Proceedings (2001), 159-174, Division of Informatics, University of Edinburgh 
16. John Harrison, Automating elementary number-theoretic proofs using Gröbner bases, CADE 21 4603 (2007), 51-66, Springer-Verlag Zbl1213.03020MR2458072
17. John Harrison, Verifying nonlinear real formulas via sums of squares, TPHOLs’2007 4732 (2007), 102-118, Springer-Verlag Zbl1144.68357MR2550881
18. John Harrison, Handbook of Practical Logic and Automated Reasoning, (2009), Cambridge University Press Zbl1178.03001MR2503047
19. Deepak Kapur, Geometry theorem proving using Hilbert’s Nullstellensatz, SYMSAC ’86 : Proceedings of the fifth ACM symposium on Symbolic and algebraic computation (1986), 202-208, ACM 
20. Deepak Kapur, A refutational approach to geometry theorem proving, Artificial Intelligence 37 (1988), 61-93 Zbl0678.68094MR987644
21. Deepak Kapur, Automated Geometric Reasoning : Dixon Resultants, Gröbner Bases, and Characteristic Sets, Automated Deduction in Geometry 1360 (1996), 1-36, Springer-Verlag Zbl0910.03010
22. Lawrence C. Paulson, Isabelle : A generic theorem prover, Journal of Automated Reasoning 828 (1994) Zbl0825.68059MR1313213
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), CEUR Workshop Proceedings 
24. Judit Robu, Geometry Theorem Proving in the Frame of the Theorema Project, (2002) Zbl0997.68130
25. Laurent Théry, A Machine-Checked Implementation of Buchberger’s Algorithm, Journal of Automated Reasoning 26 (2001) Zbl0964.03012MR1812745
26. Freek Wiedijk, Formalizing 100 Theorems Zbl1176.91039
27. Wen-Tsun Wu, On the Decision Problem and the Mechanization of Theorem-Proving in Elementary Geometry, Automated Theorem Proving - After 25 Years (1984), 213-234, American Mathematical Society Zbl0578.68078MR749248