Geodesic
Verifica automatica del ragionamento matematico
Bollettino della Unione matematica italiana, Série 8, 9A (2006) no. 3-1, pp. 361-389.

Voir la notice de l'article provenant de la source Biblioteca Digitale Italiana di Matematica

Controllare la correttezza di un ragionamento matematico, quando questo sia completamente formalizzato, è un compito che può essere delegato ad una macchina. Nasce in questo modo la Matematica Verificata al Calcolatore, una disciplina prossima alla forse più nota Dimostrazione Automatica dei Teoremi, ma da questa distinta permetodologie e obiettivi. Questo articolo si propone di presentare la verifica automatica delle dimostrazioni e di offrire alcuni spunti di riflessione sulle possibili implicazioni culturali e pratiche che questo nuovo settore di ricerca potrebbe offrire.
To check the correctness of mathematical reasoning, when it is completely formalized, is a task that can be delegated to a machine. This gives rise to the discipline of Machine Checked Mathematics, very close to the perhaps more famous Automatic Theorem Proving, but distinguished from the latter by methodologies and objectives. 
@article{BUMI_2006_8_9A_3-1_a0,
     author = {Maggesi, Marco and Simpson, Carlos},
     title = {Verifica automatica del ragionamento matematico},
     journal = {Bollettino della Unione matematica italiana},
     pages = {361--389},
     publisher = {mathdoc},
     volume = {Ser. 8, 9A},
     number = {3-1},
     year = {2006},
     zbl = {1195.03018},
     language = {it},
     url = {http://geodesic.mathdoc.fr/item/BUMI_2006_8_9A_3-1_a0/}
}
TY  - JOUR
AU  - Maggesi, Marco
AU  - Simpson, Carlos
TI  - Verifica automatica del ragionamento matematico
JO  - Bollettino della Unione matematica italiana
PY  - 2006
SP  - 361
EP  - 389
VL  - 9A
IS  - 3-1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BUMI_2006_8_9A_3-1_a0/
LA  - it
ID  - BUMI_2006_8_9A_3-1_a0
ER  - 
%0 Journal Article
%A Maggesi, Marco
%A Simpson, Carlos
%T Verifica automatica del ragionamento matematico
%J Bollettino della Unione matematica italiana
%D 2006
%P 361-389
%V 9A
%N 3-1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BUMI_2006_8_9A_3-1_a0/
%G it
%F BUMI_2006_8_9A_3-1_a0
Maggesi, Marco; Simpson, Carlos. Verifica automatica del ragionamento matematico. Bollettino della Unione matematica italiana, Série 8, 9A (2006) no. 3-1, pp. 361-389. http://geodesic.mathdoc.fr/item/BUMI_2006_8_9A_3-1_a0/

[1] AA.VV. The QED manifesto. In Proceedings of the 12th International Conference on Automated Deduction (Springer-Verlag, 1994), 238-251.

[2] The Archive of Formal Proofs. Url: http://afp.sourceforge.net/. | Zbl

[3] Jesús Aransay - Clemens Ballarin - Julio Rubio, Towards a higher reasoning level in formalized Homological Algebra. In Thérèse Hardin and Renaud Rioboo, editors, 11th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus) (Rome, Italy, 2003), 84-88. Aracne Editrice.

[4] Brian E. Aydemir - Aaron Bohannon - Matthew Fairbairn - J. Nathan Foster - Benjamin C. Pierce - Peter Sewell - Dimitrios Vytiniotis - Geoffrey Washburn - Stephanie Weirich - Steve Zdancewic, Mechanized metatheory for the masses: The PoplMark challenge. In International Conference on Theorem Proving in Higher Order Logics (TPHOLs), Lecture Notes in Computer Science. Springer Verlag, August 2005. Url: http://fling-l.seas.upenn.edu/~plclub/cgi-bin/poplmark/. | Zbl

[5] Yves Bertot - Gilles Kahn - Laurent Théry, Proof by pointing. In Theoretical aspects of computer software (Sendai, 1994), volume 789 of Lecture Notes in Comput. Sci. (Springer, Berlin, 1994), 141-160. | Zbl

[6] Alan Bundy, The Computer Modelling of Mathematical Reasoning. Academic Press, 1983. Trad. it. [7] | Zbl

[7] Alan Bundy, L'automazione del ragionamento matematico: dalla dimostrazione dei teoremi alla formazione dei concetti. Muzzio, Padova, 1986. Edizione italiana di [6] Traduzione a cura di Mauro Boscarol.

[8] Kenneth Chang, In Math, Computers Don't Lie. Or Do They? New York Times, April 6, 2004. | Zbl

[9] Alonzo Church, A formulation of the simple theory of types. Journal of Symbolic Logic, 5 (1940), 56-68. | Zbl

[10] The Coq proof assistant. Url: http://coq.inria.fr/. | Zbl

[11] J. D. Fleuriot, A Combination of Geometry Theorem Proving and Nonstandard Analysis, with Application to Newton's Principia. (Springer-Verlag, 2001). | Zbl

[12] Jacques D. Fleuriot - C. Paulson, Proving Newton's Propositio Kepleriana using geometry and nonstandard analysis in Isabelle. In Automated deduction in geometry (Beijing, 1998), volume 1669 of Lecture Notes in Comput. Sci. (Springer, Berlin, 1999), 47-66. | Zbl

[13] Jacques D. Fleuriot - Lawrence C. Paulson, Mechanizing nonstandard real analysis. LMS J. Comput. Math., 3 (electronic) (2000), 140-190. | Zbl

[14] Formal methods web page at Oxford. Url: http://www.afm.sbu.ac.uk/.

[15] Xiao Gang, WWW Interactive Multipurpose Server. Url: http://wims.unice.fr/.

[16] Freek Geuvers - Jan Herman - Randy Wiedijk - Henk Zwanenburg - Barendregt Pollack, FTA: Fundamental Theorem of Algebra Project. Url: http://www.cs.kun.nl/'freek/fta/

[17] Herman Geuvers - Freek Wiedijk - Jan Zwanenburg, A constructive proof of the Fundamental Theorem of Algebra without using the rationals. In TYPES, 2000, 96-111. | Zbl

[18] Thomas Hales, The flyspeck project. Url: http://www.math.pitt.edu/~thales/fly-speck/.

[19] John Harrison, Formalized mathematics. Technical Report 36, Turku Centre for Computer Science (TUCS), Lemminkäisenkatu 14 A, FIN-20520 Turku, Finland, 1996. Url: http://www.cl.cam.ac.uk/users/jrh/papers/form-math3.html.

[20] Gérard Huet - Amokrane Saièbi, Constructive category theory. In Proof, language, and interaction, Found. Comput. Ser., MIT Press, Cambridge, MA, 2000, 239-275.

[21] ISABELLE, Url: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/.

[22] Journal of Formalized Mathematics. Url: http://mizar.org/JFM/.

[23] L.S. Van Benthem Jutting, Checking Landau's «Grundlagen» in the AUTOMATH System. PhD thesis, Eindhoven University of Technology, 1977. | Zbl

[24] Florian Kammuèller - Lawrence C. Paulson, A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle HOL. J. Automat. Reason., 23(3-4) (1999), 235-264.

[25] D. E. Knuth - P. B. Bendix, Simple word problems in universal algebras. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970 (Springer, Berlin, Heidelberg, 1983), 342-376.

[26] Edmund Landau, Grundlagen der Analysis. Akademische Verlagsgesellschaft, Leipzig, Germany, 1930. English translation Foundations of Analysis, Chelsea Publishing Company, 1951.

[27] W. Mccune, Solution of the Robbins problem. Journal of Automated Reasoning (1997), 263-276. Url: http://www-unix.mcs.anl.gov/~mccune/papers/robbins/. | Zbl

[28] W. Mccune - R. Padmanabhan, Automated deduction in equational logic and cubic curves, volume 1095 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1996. Lecture Notes in Artificial Intelligence. | Zbl

[29] Mizar system. Url: http://mizar.uw.bialystok.pl/.

[30] Tobias Nipkow, More Church-Rosser proofs (in Isabelle/HOL). In M.A. McRobbie and J.K. Slaney, editors, Proceedings of the 13th International Conference on Automated Deduction (CADE-13), pp. 733-747, New Brunswick, New Jersey, July 1996. Springer-Verlag LNAI 1104.

[31] Tobias Nipkow - Lawrence C. Paulson - Markus Wenzel, Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. | Zbl

[32] Russell O'Connor, Proof of Gödel's first incompleteness theorem in Coq. Url: http://math.berkeley.edu/'roconnor/godel.html.

[33] Joseph Oesterlé, Densité maximale des empilements de sphéres en dimension 3 (d'après Thomas C. Hales et Samuel P. Ferguson). Astérisque, (266):Exp. No. 863, 5, 405-413, 2000. Séminaire Bourbaki, Vol. 1998/99. | fulltext EuDML

[34] Greg O'Keefe, Towards a readable formalisation of category theory. Electronic Notes in Theoretical Computer Science, 91:212--228, February 2004. | Zbl

[35] OTTER, An automated deduction system. Url: http://www-unix.mcs.anl.gov/AR/otter/.

[36] R. Padmanabhan - W. Mccune, An Equational Characterization of the Conic Construction on Cubic Curves. Number 1095 in Lecture Notes in Computer Science (AI subseries). Springer-Verlag, 1996.

[37] William Padmanabhan - R. Mccune, Automated Deduction in Equational Logic and Cubic Curves (Springer Verlag, 1996). | Zbl

[38] Lawrence C. Paulson, The relative consistency of the axiom of choice mechanized using Isabelle/ZF. LMS J. Comput. Math., 6 (electronic) (2003), 198-248. Appendix A available electronically at http://www.lms.ac.uk/jcm/6/lms2003-001/appendix-a/ | Zbl

[39] Proof and beauty. The Economist, marzo 2005.

[40] C. Raffalli, The PhoX proof assistant. Url: http://www.lama.univ-savoie.fr/'raffalli/phox.html.

[41] Christophe Raffalli - René David, Computer assisted teaching in mathematics. In Workshop on 35 years of Automath (Avril 2002, Edingurgh), 2002.

[42] Carlos T. Simpson, Computer theorem proving in math, 2003. arXiv:math.HO/0311260.

[43] Carlos T. Simpson, Set-theoretical mathematics in Coq, 2004. arXiv:math.LO/0402336.

[44] Laurent Théry, A machine-checked implementation of Buchberger's algorithm. J. Automat. Reason., 26(2) (2001), 107-137. | Zbl

[45] Freek Wiedijk, Comparing mathematical provers. In Andrea Asperti, Bruno Buchberger, and James Davenport, editors, Mathematical Knowledge Management, number 2594 in Lecture Notes on Computer Science, pp 188-202. Springer, 2003. Proceedings of MKM 2003. | Zbl

[46] Larry Wos - Dolph Ulrich - Branden Fitelson, Vanquishing the XCB Question: The Methodological Discovery of the Last Shortest Single Axiom for the Equivalential Calculus. Journal of Automated Reasoning, 29(2) (2002), 107-124. | Zbl