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.
Referenze Bibliografiche
[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] 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 1152.68516[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 0942.03504[6]
ALAN BUNDY,
The Computer Modelling of Mathematical Reasoning.
Academic Press,
1983. Trad. it. [7] |
Zbl 0541.68067[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 1065.68616[9]
ALONZO CHURCH,
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]
J. D. FLEURIOT,
A Combination of Geometry Theorem Proving and Nonstandard Analysis, with Application to Newton's Principia. (
Springer-Verlag,
2001). |
Zbl 0976.68133[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 0952.03004[13]
JACQUES D. FLEURIOT -
LAWRENCE C. PAULSON,
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] 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 1054.03041[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 0352.68105[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 0883.06011[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 0921.03011[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 0994.68131[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 1271.68213[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 0921.03011[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 1053.03009[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 0964.03012[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 1022.68623[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 1020.03006
Con il contributo del Ministero per i Beni e le Attività Culturali