Mathematics is a precise discipline, but mathematical rigor is not the same as logical formality. When one tries to translate a mathematical argument to a format suited for automated processing, one realizes that there is a tangible mismatch between a text-book presentation and what is actually required by the machine. Ordinary mathematics is simply too informal for the logical and algebraic procedures that contemporary au- tomated reasoning has to offer. At a linguistic level, ordinary mathematical discourse systematically overloads symbols and abuses notations in ways that make mechanical interpretation difficult. Subtle contextual cues are needed to resolve the ambiguities that are intrinsic to mathematical vernacular, requiring not just knowledge of the notation and conventions at play but, moreover, an understanding of the relevant mathematical discipline.

A. Asperti, J.Avigad (2011). Zen and the art of formalisation. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 21(4), 679-682 [10.1017/S0960129511000065].

Zen and the art of formalisation.

ASPERTI, ANDREA;
2011

Abstract

Mathematics is a precise discipline, but mathematical rigor is not the same as logical formality. When one tries to translate a mathematical argument to a format suited for automated processing, one realizes that there is a tangible mismatch between a text-book presentation and what is actually required by the machine. Ordinary mathematics is simply too informal for the logical and algebraic procedures that contemporary au- tomated reasoning has to offer. At a linguistic level, ordinary mathematical discourse systematically overloads symbols and abuses notations in ways that make mechanical interpretation difficult. Subtle contextual cues are needed to resolve the ambiguities that are intrinsic to mathematical vernacular, requiring not just knowledge of the notation and conventions at play but, moreover, an understanding of the relevant mathematical discipline.
2011
A. Asperti, J.Avigad (2011). Zen and the art of formalisation. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 21(4), 679-682 [10.1017/S0960129511000065].
A. Asperti; J.Avigad
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/105044
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 0
social impact