The recent achievements obtained by means of Interactive Theorem Provers in the automatic verification of complex mathematical results have reopened an old and interesting debate about the essence and purpose of proofs, emphasizing the dichotomy between message and certificate. We claim that it is important to prevent the divorce between these two epistemological functions, discussing the implications for the field of mathematical knowledge management.
Andrea Asperti (2012). Proof, Message and Certificate. Springer Verlag.
Proof, Message and Certificate
ASPERTI, ANDREA
2012
Abstract
The recent achievements obtained by means of Interactive Theorem Provers in the automatic verification of complex mathematical results have reopened an old and interesting debate about the essence and purpose of proofs, emphasizing the dichotomy between message and certificate. We claim that it is important to prevent the divorce between these two epistemological functions, discussing the implications for the field of mathematical knowledge management.File in questo prodotto:
Eventuali allegati, non sono esposti
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
