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_361_0,
author = {Marco Maggesi and Carlos Simpson},
title = {Verifica automatica del ragionamento matematico},
journal = {Bollettino dell'Unione Matematica Italiana},
volume = {9-A},
year = {2006},
pages = {361-389},
zbl = {1195.03018},
mrnumber = {2309896},
language = {it},
url = {http://dml.mathdoc.fr/item/BUMI_2006_8_9A_3-1_361_0}
}
Maggesi, Marco; Simpson, Carlos. Verifica automatica del ragionamento matematico. Bollettino dell'Unione Matematica Italiana, Tome 9-A (2006) pp. 361-389. http://gdmltest.u-ga.fr/item/BUMI_2006_8_9A_3-1_361_0/
[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 06512407
[3] - - , Towards a higher reasoning level in formalized Homological Algebra. In and , editors, 11th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus) (Rome, Italy, 2003), 84-88. Aracne Editrice.
[4] - - - - - - - - - , 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 1152.68516
[5] - - , 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 0942.03504
[6] , The Computer Modelling of Mathematical Reasoning. Academic Press, 1983. Trad. it. [7] | Zbl 0541.68067
[7] , 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] , In Math, Computers Don't Lie. Or Do They?New York Times, April 6, 2004. | Zbl 1065.68616
[9] , A formulation of the simple theory of types. Journal of Symbolic Logic, 5 (1940), 56-68. | Zbl 0023.28901
[10] The Coq proof assistant. Url: http://coq.inria.fr/. | Zbl 1138.68525
[11] , A Combination of Geometry Theorem Proving and Nonstandard Analysis, with Application to Newton's Principia. (Springer-Verlag, 2001). | Zbl 0976.68133
[12] - , 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 0952.03004
[13] - , Mechanizing nonstandard real analysis. LMS J. Comput. Math., 3 (electronic) (2000), 140-190. | Zbl 0951.03006
[14] Formal methods web page at Oxford. Url: http://www.afm.sbu.ac.uk/.
[15] , WWW Interactive Multipurpose Server. Url: http://wims.unice.fr/.
[16] - - - - , FTA: Fundamental Theorem of Algebra Project. Url: http://www.cs.kun.nl/'freek/fta/
[17] - - , A constructive proof of the Fundamental Theorem of Algebra without using the rationals. In TYPES, 2000, 96-111. | Zbl 1054.03041
[18] , The flyspeck project. Url: http://www.math.pitt.edu/~thales/fly-speck/.
[19] , 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] - , 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] , Checking Landau's «Grundlagen» in the AUTOMATH System. PhD thesis, Eindhoven University of Technology, 1977. | Zbl 0352.68105
[24] - , 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] - , Simple word problems in universal algebras. In and , editors, Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970 (Springer, Berlin, Heidelberg, 1983), 342-376.
[26] , Grundlagen der Analysis. Akademische Verlagsgesellschaft, Leipzig, Germany, 1930. English translation Foundations of Analysis, Chelsea Publishing Company, 1951.
[27] , Solution of the Robbins problem. Journal of Automated Reasoning (1997), 263-276. Url: http://www-unix.mcs.anl.gov/~mccune/papers/robbins/. | Zbl 0883.06011
[28] - , 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 0921.03011
[29] Mizar system. Url: http://mizar.uw.bialystok.pl/.
[30] , More Church-Rosser proofs (in Isabelle/HOL). In and , 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] - - , Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. | Zbl 0994.68131
[32] , Proof of Gödel's first incompleteness theorem in Coq. Url: http://math.berkeley.edu/'roconnor/godel.html.
[33] , 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] , Towards a readable formalisation of category theory. Electronic Notes in Theoretical Computer Science, 91:212--228, February 2004. | Zbl 1271.68213
[35] OTTER, An automated deduction system. Url: http://www-unix.mcs.anl.gov/AR/otter/.
[36] - , An Equational Characterization of the Conic Construction on Cubic Curves. Number 1095 in Lecture Notes in Computer Science (AI subseries). Springer-Verlag, 1996.
[37] - , Automated Deduction in Equational Logic and Cubic Curves (Springer Verlag, 1996). | Zbl 0921.03011
[38] , 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 1053.03009
[39] Proof and beauty. The Economist, marzo 2005.
[40] , The PhoX proof assistant. Url: http://www.lama.univ-savoie.fr/'raffalli/phox.html.
[41] - , Computer assisted teaching in mathematics. In Workshop on 35 years of Automath (Avril 2002, Edingurgh), 2002.
[42] , Computer theorem proving in math, 2003. arXiv:math.HO/0311260.
[43] , Set-theoretical mathematics in Coq, 2004. arXiv:math.LO/0402336.
[44] , A machine-checked implementation of Buchberger's algorithm. J. Automat. Reason., 26(2) (2001), 107-137. | Zbl 0964.03012
[45] , Comparing mathematical provers. In , , and , editors, Mathematical Knowledge Management, number 2594 in Lecture Notes on Computer Science, pp 188-202. Springer, 2003. Proceedings of MKM 2003. | Zbl 1022.68623
[46] - - , 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 1020.03006