La Stampa - Consultazione Archivio

Computer come Euclide? Computer come Euclide? Un teorema dimostrato «a macchina» grado di determinare milioni di teoremi deducibili da un dato insieme di ipotesi. In verità finora i dimostratori automatici di teoremi non hanno portato contributi rivoluzionari al progresso della matematica o di altre discipline scientifiche. Sono rapidissimi nel dedurre nuovi teoremi, ma incapaci di identificare, nei milioni di nuovi teoremi proposti in pochi passi di deduzione, quali debbano essere selezionati come pietre miliari per il progresso scientifico. Il primo risultato importante ottenuto da un «theorem prover» è la dimostrazione, nel 1976, del teorema dei quattro colori (che risale al lontano 1853). Il problema proposto riguardava la possibilità di colorare una carta geografica con quattro colori, in modo che regioni con cor ~jiì in comune non avessero mai lo stesso colore. La dimostrazione suggerita dal calcolatore 120 anni dopo la prima formulazione della congettura, fu però oggetto di molte riflessioni critiche perché basata su molta intelligenza naturale dispiegata nell'impostazione della dimostrazione. Ora, la svolta. William McCune e Larry Wos, dell'Argonne portante nel mondo della ricerca, Herbert Robbins, aveva suggerito la sostituzione della terza di queste equazioni con una relazione più semplice, senza tuttavia riuscire a dimostrare che la nuova terna di equazioni fosse sufficiente a definire un'algebra Booleana. Risparmio al lettore il confronto delle equazioni di Huntington e Robbins, perché troppo ermetico per i non addetti ai lavori. Inoltre, a giudizio del sottoscritto, la congettura di Robbins non è molto importante dal punto di vista scientifico ed ha una rilevanza applicativa ancora inferiore a quella concettuale. L'importanza di quell'algebra di Boole dal punto di vista della logica, ossia la possibilità di attribuire alle sue operazioni elementari di somma, prodotto e complementazione il significato di «oppure», «e inoltre» e «non» nelle valutazioni della verità o falsità delle proposizioni, era stata ampiamente analizzata, a metà del secolo scorso, dal suo ideatore George Boole, che aveva introdotto quel calcolo come strumento di base per «l'analisi delle leggi del pensiero». L'importanza della notizia non è nelle sue implicazioni per National Laboratory in Illinois, hanno annunciato di aver dimostrato la congettura di Robbins con l'impiego completamente automatico di un loro «theorem prover» assolutamente generale e non con un programma sviluppato specificatamente per quella dimostrazione. La congettura di Robbins riguarda la terza di un insieme di tre equazioni che esprimono le condizioni necessarie e sufficienti perché un'algebra sia Booleana. Nel 1933 Huntington aveva proposto tre equazioni di base, ma un suo studente, destinato a divenire una personalità im¬