Verifica automatica del ragionamento matematico
Bollettino della Unione matematica italiana, Série 8, 9A (2006) no. 3-1, pp. 361-389
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_a0,
author = {Maggesi, Marco and Simpson, Carlos},
title = {Verifica automatica del ragionamento matematico},
journal = {Bollettino della Unione matematica italiana},
pages = {361--389},
year = {2006},
volume = {Ser. 8, 9A},
number = {3-1},
zbl = {1195.03018},
mrnumber = {MR2309896},
language = {it},
url = {http://geodesic.mathdoc.fr/item/BUMI_2006_8_9A_3-1_a0/}
}
Maggesi, Marco; Simpson, Carlos. Verifica automatica del ragionamento matematico. Bollettino della Unione matematica italiana, Série 8, 9A (2006) no. 3-1, pp. 361-389. http://geodesic.mathdoc.fr/item/BUMI_2006_8_9A_3-1_a0/