Presentazione
di Marcello D'Agostino
Università di Ferrara

Negli anni ’30 del XX secolo Gerhard Gentzen avviò una vera e propria “rivoluzione copernicana” nel campo della logica. La ricerca era stata fino ad allora dominata dal cosiddetto “metodo assiomatico”: l’insieme delle verità logiche (le “tautologie” nella terminologia di Wittgenstein, ossia le proposizioni “vere in tutti i mondi possibili”) venivano derivate, attraverso determinate regole di “manipolazione dei simboli”, da un insieme limitato di verità logiche primitive prese come “assiomi”, un modo certamente innaturale di formalizzare le argomentazioni deduttive che si incontrano nel ragionamento scientifico e in quello ordinario. Nel tentativo di riavvicinare i formalismi della logica all’effettiva pratica deduttiva, Gentzen elaborò un nuovo tipo di calcolo logico – la cosiddetta “deduzione naturale” - in cui è possibile formalizzare direttamente qualunque deduzione secondo “regole di inferenza” che ricalcano formalmente le tipiche argomentazioni utilizzate nel ragionamento matematico. Introdusse anche una variante tecnica di questo metodo (il cosiddetto “calcolo dei sequenti”) che gli consentì di dimostrare una proprietà molto importanti, come il “teorema della sottoformula” - “nella dimostrazione non rientra alcun concetto [formula] che non sia contenuto nel suo risultato finale [il teorema da dimostrare]”(Gentzen, 1935). Il risultato di Gentzen, contenuto nel suo celebre “teorema di eliminazione del taglio” consentiva di limitare drasticamente lo spazio di ricerca di una dimostrazione in modo da renderne più agevole l’esplorazione da parte di una procedura meccanica. Negli anni ’60 e ’70 i calcoli di Gentzen furono perciò fra i primi ad essere utilizzati in quel settore dell’Intelligenza Artificiale noto come “deduzione automatica”. Tuttavia l’avvento dei calcolatori digitali aveva determinato un drammatico cambiamento di scenario. La possibilità effettiva, e non più solo teorica, di meccanizzare la ricerca di una dimostrazione sollevava problemi nuovi, primo fra tutti il problema dell’efficienza. Sebbene in teoria il teorema di Gentzen consentisse di ridurre lo spazio di ricerca delle dimostrazioni a proporzioni governabili (nel caso della logica proposizionale a proporzioni finite), in pratica ci si rese presto conto che il numero di possibilità è talmente enorme da generare una vera e propria “esplosione combinatoria”, rendendo le procedure di ricerca praticamente inutili. Sebbene certi algoritmi siano in grado eseguire in linea di principio qualunque ragionamento logico, di fatto sono catastroficamente inefficienti – persino un computer ultraveloce ci mettere diversi secoli a dare una risposta - e dunque non ci forniscono alcuna soluzione reale. Di più, la congettura dominante fra gli scienziati è che non esista nessuna procedura meccanica davvero efficiente, ossia tale da non condurre a un’esplosione combinatoria, neppure nel dominio limitato della logica proposizionale.
Era questo lo sfondo teorico dell’articolo “The Taming of the Cut” pubblicato sul Journal of Logic and Computation nel 1994. Già da diversi anni Marco Mondadori lavorava allo sviluppo di una serie di nuovi calcoli logici che fossero più adeguati dei metodi di Gentzen a formalizzare i ragionamenti deduttivi “classici” (quelli basati sulle dimostrazioni per assurdo) e le cui regole rappresentassero in modo più adeguato il significato classico degli “operatori logici”. Per una sorta di armonia prestabilita lo studio di questi problemi filosofici di teoria del significato mostrò di avere interessanti conseguenze rispetto a un problema eminentemente pratico come quello dell’efficienza computazionale. Dopo qualche anno emerse che uno di questi calcoli (chiamato KE) - per quanto inevitabilmente soggetto come tutti gli altri al fenomeno dell’esplosione combinatoria - era tuttavia molto più efficiente di altri metodi diffusamente impiegati nelle applicazioni informatiche, nel senso che consentiva di eseguire in pratica (tecnicamente in “tempo polinomiale”) ampie classi di deduzioni che negli altri calcoli risultavano “intrattabili” (ossia la cui esecuzione richiedeva un tempo “esponenziale”). Da allora KE ha conquistato un posto stabile nella ricerca sulla deduzione automatica ed è anche largamente utilizzato nella didattica della logica.