Alan Bundy,
“L’AUTOMAZIONE DEL RAGIONAMENTO MATEMATICO – Dalla
dimostrazione dei teoremi alla formazione dei concetti”, IAR
4 (Intelligenza Artificiale e Robotica), Edizione italiana a cura
di Mauro Boscarol, 425 pagine, franco muzzio editore, Prima edizione:
luglio 1986
Alan Bundy è
ricercatore in intelligenza artificiale presso il Department of
Artificial Intelligence dell’Università di Edinburgo.
Dalla quarta
di copertina: “Questo libro descrive programmi per computer che fanno
matematica, nel senso che dimostrano teoremi, elaborano modelli
matematici o scoprono nuovi concetti matematici.[…]"
Nella Prefazione
di Alan Bundy, datata Maggio 1983, si legge: “Questo libro è
nato da una serie di appunti per un corso post-laurea in Ragionamento
matematico tenuto al Dipartimento di Intelligenza Artificiale a Edinburgo
dal 1979 in poi. Gli studenti del corso avevano formazioni molto diverse:
psicologia, informatica, matematica, didattica, eccetera. La prima stesura
degli appunti è stata scritta durante un permesso sabbatico di un
trimestre nel 1980. Più avanti gli appunti sono stati utili per un corso
simile a livello pre laurea. […]
Non è
necessario essere un matematico professionista o un informatico per
leggere questo libro, ma tuttavia il libro presuppone qualche conoscenza
matematica. Per esempio è necessario sapere cosa siano un insieme e un
gruppo. […]"
-
Il
capitolo 1 è una introduzione generale: motiva il soggetto e dà
alcune informazioni storiche. (Viene subito precisato che il libro è
diretto alle persone interessate alla domanda come si fa la
matematica?, cioè ai matematici professionisti, agli psicologi
che studiano il ragionamento matematico e a chiunque abbia curiosità
sull’apparentemente misterioso processo con cui i matematici
congetturano teoremi, formulano definizioni, costruiscono
dimostrazioni e realizzano modelli matematici. La tesi dell’autore
è che si possa gettare luce su questo “misterioso” processo, con
l’aiuto di uno strumento meraviglioso, il computer.)
-
La prima
parte è una introduzione in tre capitoli alla logica matematica;
descrive solo quegli aspetti della logica che sono necessari per
comprendere il resto del libro.
-
La
seconda parte è una introduzione in tre capitoli alla dimostrazione
di teoremi mediante risoluzione.
-
La terza
parte consiste di cinque ricostruzioni razionali di tecniche o
programmi di dimostrazione automatica. Ognuno di essi è stato scelto
perché contribuisce in modo importante, anche se parziale, alla soluzione
del problema di guidare la ricerca di una dimostrazione. Questa parte
è il nucleo del libro.
-
La quarta
parte è una discussione in due capitoli degli aspetti del
ragionamento matematico diversi dalla dimostrazione di teoremi, anche
se alla fine si riducono ambedue alla dimostrazione di teoremi.
-
La quinta
parte è una investigazione in tre capitoli degli aspetti più
matematici della dimostrazione automatica, per esempio le
dimostrazioni di completezza. Può essere omessa da coloro che non
hanno solidi fondamenti in matematica.
-
L’ultimo
capitolo discute alcune applicazioni delle tecniche descritte nel
libro, dalla manipolazione algebrica alla didattica.
-
Le
appendici comprendono: programmi per computer, una discussione sulla
notazione, le soluzioni degli esercizi e la bibliografia.
|