Ultimo aggiornamento: 07/11/2005

 
     

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.