OliForum Matematico

Siete appassionati di dimostratori automatici ?
Se sì, qual'è il vostro dimostratore automatico (o proof checker) preferito ?
Il mio programma preferito è Mizar; sembra poco potente, ma alla fine mi sono convinto che, in confronto agli altri, fa quasi miracoli. Ha una bellissima libreria e i programmi sono leggibili.

Possibile che a nessuno interessi l'argomento ? Sono l'unico ad aver sperato nell'esistenza di un super-programma che trova le dimostrazioni da solo ?

chissà forse trovare una dimostrazione da soli senza l'aiuto di un computer da qualche soddisfazione in più...

Si vede che non ne hai mai usato uno...
Trovare una dimostrazione con i dimostratori automatici è più difficile che scriverne una a mano.
A pensarci bene, deve essere questo che li rende così poco popolari...

Non è che potresti spiegare di cosa si tratta?

Grazie Anlem, per fortuna che ci sei tu a mostrare interesse
Allora, l'idea originaria sarebbe costruire programmi che fanno matematica il più possibile da soli, per esempio trovare dimostrazioni, ecc...
Il problema è che, a mano a mano che gli assiomi aumentano e si intrecciano (cioè praticamente in tutte le teorie matematiche e i problemi un po' interessanti, dalla teoria dei numeri, alla geometria euclidea) i dimostratori automatici "puri" si dimostrano decisamente limitati. Esempi di dimostratori automatici puri sono, per esempio, Otter ed E (si chiama così...). Nel 1997 con Otter sono riusciti a dimostrare una congettura abbastanza famosa in algebra booleana risalente agli anni '30. La dimostrazione è stata totalmente automatica, ma la cosa ha funzionato proprio perchè si può descrivere il problema con pochissimi assiomi nella logica del primo ordine.
La ricerca continua, ma i più "realisti" si sono accontentati, invece di creare un "super-programma" universale, di costruire programmi che potessero controllare una dimostrazione e che fossero in grado di risparmiare all'utente di scrivere i passaggi banali. Questo tipo di programmi si chiama proof checker. Per esempio, nel 1998 Hales ha dimostrato la cosiddetta congettura di Keplero, ma, poichè ci sono degli scettici, per tutta una serie di motivi, ha deciso di scrivere una dimostrazione su un proof checker di nome "HOL Light".
Poi, ci sono programmi che stanno a metà tra proof-checker e dimostratori automatici, che servono per le cosiddette dimostrazioni assistite al calcolatore, dove l'utente cerca di "indovinare" la strategia giusta, cioè i suggerimenti giusti da dare al programma, perchè il programma trovi la dimostrazione. La cosa non è molto facile, ci vuole esperienza, cioè pratica.
Il mondo dei dimostratori è amplissimo, perchè ci sono tantissimi programmi, ognuno con una sua sintassi particolare e, soprattutto, con una sua logica (per esempio, la base può essere data dalla logica di ordine superiore, dalla logica intuizionista, dalla logica classica, dalla teoria di Martin-Lof, dalle funzioni primitive ricorsive...).
Per gli interessati, a questo punto consiglio questa pagina web:
http://www.cs.ru.nl/~freek/