Verifica automatica del ragionamento matematico

Marco Maggesi; Carlos Simpson

Bollettino dell'Unione Matematica Italiana (2006)

  • Volume: 9-A, Issue: 3-1, page 361-389
  • ISSN: 0392-4041

Abstract

top
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.

How to cite

top

Maggesi, Marco, and Simpson, Carlos. "Verifica automatica del ragionamento matematico." Bollettino dell'Unione Matematica Italiana 9-A.3-1 (2006): 361-389. <http://eudml.org/doc/289559>.

@article{Maggesi2006,
abstract = {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.},
author = {Maggesi, Marco, Simpson, Carlos},
journal = {Bollettino dell'Unione Matematica Italiana},
language = {ita},
month = {12},
number = {3-1},
pages = {361-389},
publisher = {Unione Matematica Italiana},
title = {Verifica automatica del ragionamento matematico},
url = {http://eudml.org/doc/289559},
volume = {9-A},
year = {2006},
}

TY - JOUR
AU - Maggesi, Marco
AU - Simpson, Carlos
TI - Verifica automatica del ragionamento matematico
JO - Bollettino dell'Unione Matematica Italiana
DA - 2006/12//
PB - Unione Matematica Italiana
VL - 9-A
IS - 3-1
SP - 361
EP - 389
AB - 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.
LA - ita
UR - http://eudml.org/doc/289559
ER -

References

top
  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/. Zbl06512407
  3. ARANSAY, JESÚS - BALLARIN, CLEMENS - RUBIO, JULIO, 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. AYDEMIR, BRIAN E. - BOHANNON, AARON - FAIRBAIRN, MATTHEW - FOSTER, J. NATHAN - PIERCE, BENJAMIN C. - SEWELL, PETER - VYTINIOTIS, DIMITRIOS - WASHBURN, GEOFFREY - WEIRICH, STEPHANIE - ZDANCEWIC, STEVE, 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/. Zbl1152.68516
  5. BERTOT, YVES - KAHN, GILLES - THÉRY, LAURENT, Proof by pointing. In Theoretical aspects of computer software (Sendai, 1994), volume 789 of Lecture Notes in Comput. Sci. (Springer, Berlin, 1994), 141-160. Zbl0942.03504
  6. BUNDY, ALAN, The Computer Modelling of Mathematical Reasoning. Academic Press, 1983. Trad. it. [7] Zbl0541.68067
  7. BUNDY, ALAN, 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. CHANG, KENNETH, In Math, Computers Don't Lie. Or Do They?New York Times, April 6, 2004. Zbl1065.68616
  9. CHURCH, ALONZO, A formulation of the simple theory of types. Journal of Symbolic Logic, 5 (1940), 56-68. Zbl0023.28901
  10. The Coq proof assistant. Url: http://coq.inria.fr/. Zbl1138.68525
  11. FLEURIOT, J. D., A Combination of Geometry Theorem Proving and Nonstandard Analysis, with Application to Newton's Principia. (Springer-Verlag, 2001). Zbl0976.68133
  12. FLEURIOT, JACQUES D. - PAULSON, C., 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. Zbl0952.03004
  13. FLEURIOT, JACQUES D. - PAULSON, LAWRENCE C., Mechanizing nonstandard real analysis. LMS J. Comput. Math., 3 (electronic) (2000), 140-190. Zbl0951.03006
  14. Formal methods web page at Oxford. Url: http://www.afm.sbu.ac.uk/. 
  15. GANG, XIAO, WWW Interactive Multipurpose Server. Url: http://wims.unice.fr/. 
  16. GEUVERS, FREEK - HERMAN, JAN - WIEDIJK, RANDY - ZWANENBURG, HENK - POLLACK, BARENDREGT, FTA: Fundamental Theorem of Algebra Project. Url: http://www.cs.kun.nl/'freek/fta/ 
  17. GEUVERS, HERMAN - WIEDIJK, FREEK - ZWANENBURG, JAN, A constructive proof of the Fundamental Theorem of Algebra without using the rationals. In TYPES, 2000, 96-111. Zbl1054.03041
  18. HALES, THOMAS, The flyspeck project. Url: http://www.math.pitt.edu/~thales/fly-speck/. 
  19. HARRISON, JOHN, 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. HUET, GÉRARD - SAIÈBI, AMOKRANE, 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. VAN BENTHEM JUTTING, L.S., Checking Landau's «Grundlagen» in the AUTOMATH System. PhD thesis, Eindhoven University of Technology, 1977. Zbl0352.68105
  24. KAMMUÈLLER, FLORIAN - C. PAULSON, LAWRENCE, 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. KNUTH, D. E. - BENDIX, P. B., 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. LANDAU, EDMUND, Grundlagen der Analysis. Akademische Verlagsgesellschaft, Leipzig, Germany, 1930. English translation Foundations of Analysis, Chelsea Publishing Company, 1951. 
  27. MCCUNE, W., Solution of the Robbins problem. Journal of Automated Reasoning (1997), 263-276. Url: http://www-unix.mcs.anl.gov/~mccune/papers/robbins/. Zbl0883.06011
  28. MCCUNE, W. - PADMANABHAN, R., 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. Zbl0921.03011
  29. Mizar system. Url: http://mizar.uw.bialystok.pl/. 
  30. NIPKOW, TOBIAS, 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-VerlagLNAI1104. 
  31. NIPKOW, TOBIAS - PAULSON, LAWRENCE C. - WENZEL, MARKUS, Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Zbl0994.68131
  32. O'CONNOR, RUSSELL, Proof of Gödel's first incompleteness theorem in Coq. Url: http://math.berkeley.edu/'roconnor/godel.html. 
  33. OESTERLÉ, JOSEPH, 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. 
  34. O'KEEFE, GREG, Towards a readable formalisation of category theory. Electronic Notes in Theoretical Computer Science, 91:212--228, February 2004. Zbl1271.68213
  35. OTTER, An automated deduction system. Url: http://www-unix.mcs.anl.gov/AR/otter/. 
  36. PADMANABHAN, R. - MCCUNE, W., An Equational Characterization of the Conic Construction on Cubic Curves. Number 1095 in Lecture Notes in Computer Science (AI subseries). Springer-Verlag, 1996. 
  37. PADMANABHAN, WILLIAM - MCCUNE, R., Automated Deduction in Equational Logic and Cubic Curves (Springer Verlag, 1996). Zbl0921.03011
  38. PAULSON, LAWRENCE C., 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/ Zbl1053.03009
  39. Proof and beauty. The Economist, marzo 2005. 
  40. RAFFALLI, C., The PhoX proof assistant. Url: http://www.lama.univ-savoie.fr/'raffalli/phox.html. 
  41. RAFFALLI, CHRISTOPHE - DAVID, RENÉ, Computer assisted teaching in mathematics. In Workshop on 35 years of Automath (Avril 2002, Edingurgh), 2002. 
  42. SIMPSON, CARLOS T., Computer theorem proving in math, 2003. arXiv:math.HO/0311260. 
  43. SIMPSON, CARLOS T., Set-theoretical mathematics in Coq, 2004. arXiv:math.LO/0402336. 
  44. THÉRY, LAURENT, A machine-checked implementation of Buchberger's algorithm. J. Automat. Reason., 26(2) (2001), 107-137. Zbl0964.03012
  45. WIEDIJK, FREEK, 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. Zbl1022.68623
  46. WOS, LARRY - ULRICH, DOLPH - FITELSON, BRANDEN, 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. Zbl1020.03006

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.