Dimostrazione automatica di teoremi

La dimostrazione automatica di teoremi (in inglese Automated theorem proving o ATP) o deduzione automatica, è il sottocampo più sviluppato del ragionamento automatico. L'operazione consiste nella dimostrazione di teoremi matematici da parte di un programma per computer.

Definizione

Le tecniche di computazione automatica di un teorema consistono nell'applicazione di metodi computazionali alla dimostrazione dei teoremi. In generale, la procedura è la seguente:

1. Il teorema da dimostrare si converte in termini algebrici: sia l'ipotesi che la tesi sono espresse come condizioni del tipo $P_{i}(x_{1},\ldots ,x_{n})=0,i=1,\ldots ,k$ e $Q(x_{1},\ldots ,x_{n})=0$ rispettivamente.
2. La veridicità del teorema è quindi equivalente a quello $Q\,$ è nell'ideale generato da $P_{1},\ldots ,P_{k}$ (equivalente al l'annullamento di $P_{1},\ldots ,P_{k}$ in un dato punto comporta l'annullamento di $Q\,$ in quello stesso punto).

Tuttavia quello dell'appartenenza di un polinomio ad un ideale è un classico problema dell'Algebra computazionale; una tecnica comune per risolvere questo problema è il calcolo di una base Gröbner adeguata. Questo metodo ha lo svantaggio di un'elevata complessità computazionale.

Evoluzione storica

Mentre le radici della logica formalizzata risalgono a Aristotele, è il periodo tra la fine del XIX e l'inizio del XX secolo che ha visto lo sviluppo della logica moderna e della matematica formalizzata.

Gottlob Frege in Begriffsschrift (1879) ha introdotto sia un calcolo proposizionale completo che una logica dei predicati essenzialmente moderna. I suoi Die Grundlagen der Arithmetik (Fondamenti di aritmetica), pubblicati nel 1884, hanno espresso parti di matematica in logica formale.

Questo approccio è stato continuato da Russell e Whitehead nella loro influente opera Principia Mathematica, pubblicata per la prima volta tra il 1910 e il 1913 e con una seconda edizione rivista nel 1927. Russell e Whitehead pensarono di poter derivare tutte le verità matematiche usando assiomi e regole di inferenza di logica formale, iniziando in linea di principio il processo all'automazione.

Nel 1920 Thoralf Skolem semplificò un precedente risultato di Leopold Löwenheim, portando al teorema di Löwenheim-Skolem e, nel 1930, alla nozione di un Universo di Herbrand e di Interpretazione di Herbrand che consentiva di ridurre il soddisfacimento (o meno) delle formule di primo ordine (e quindi la validità di un teorema) a più (potenzialmente infiniti) problemi di soddisfacimento in termini proposizionali.

Nel 1929 Mojżesz Presburger mostrò che la teoria dei numeri naturali con addizione e uguaglianza (oggi chiamata aritmetica di Presburger in suo onore) è decidibile e ha fornito un algoritmo in grado di determinare se una determinata frase nella lingua fosse vera o falsa.

Tuttavia, poco dopo questo risultato positivo, Kurt Gödel nel 1931 pubblicò Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I (Sulle Proposizioni formalmente indecidibili dei principi di matematica e sistemi correlati), dimostrando che in qualsiasi sistema assiomatico sufficientemente potente esistono affermazioni vere che non possono essere dimostrate all'interno del sistema. Quest'argomento è stato ulteriormente sviluppato negli anni Trenta del XX secolo da Alonzo Church e Alan Turing, che da un lato hanno dato due definizioni indipendenti ma equivalenti di computabilità, e dall'altro hanno fornito esempi concreti di problemi indecidibili.

Poco dopo la seconda guerra mondiale, sono diventati disponibili i primi computer. Nel 1954, Martin Davis programmò l'algoritmo di Presburger per un computer a valvole termoioniche JOHNNIAC presso l'Istituto per gli studi avanzati di Princeton. Secondo Davis, "il suo grande trionfo era quello di dimostrare che la somma di due numeri pari è pari".

Più ambiziosa era la Logic Theorist, un programma di deduzione per logica proposizionale dei Principia Mathematica, sviluppata da Allen Newell, Herbert A. Simon e J. C. Shaw. Inoltre il Logic Theorist,in esecuzione sul JOHNNIAC, ha costruito dimostrazioni da una piccola serie di assiomi proposizionali e da tre regole di deduzione: il modus ponens, la sostituzione di una variabile proposizionale e la sostituzione delle formule con la loro definizione. Il sistema ha utilizzato la guida euristica e ha saputo dimostrare 38 dei primi 52 teoremi dei Principia.

L'approccio "euristico" del sistema del Logic Theorist ha cercato di emulare i matematici umani e non ha potuto garantire che una dimostrazione possa essere trovata per ogni teorema valido, neanche in linea di principio. Al contrario, altri algoritmi più sistematici hanno raggiunto, almeno teoricamente, la completezza per la logica del primo ordine. Gli approcci iniziali si basavano sui risultati di Herbrand e Skolem per convertire una formula di primo ordine in gruppi successivamente più grandi di formule proposizionali, istanziando le variabili con termini dell'universo Herbrand. L'inadeguatezza delle formule proposizionali potrebbe essere verificata utilizzando un certo numero di metodi. Il programma di Gilmore ha utilizzato la conversione in forma normale disgiuntiva, una forma in cui è sufficiente la soddisfazione di una formula.

Voci correlate

• Ragionamento automatico

Controllo di autorità	LCCN (EN) sh85010111 · J9U (EN, HE) 987007295721005171