Interactive theorem prover

[hamming_burst]

Salve,
chiedo a qualche matematico/logico un'opinione.

Conscete percaso i tool che permettono di "dimostrare" teoremi in modo interattivo, tramite un meta-linguaggio?
Se sì, che ne pensate, li ritenete utili?

I tool che intendo sono tipo:
- Isabelle
- Coq

Se qualcuno vorrà rispondere,

RIngrazio

[hamming_burst]

"Deckard":E quindi se coq ci dice che la dimostrazione è esatta, ma noi non siamo in grado di afferrarla, a che serve tutto ciò?

E' una delle domande che mi son posto quando me lo hanno mostrato.
Con una sola proposizione logica, con un'implicazione ed un and, bisogna scrivere righe e righe del linguaggio di Coq, e poi hai una scritta con "teorema dimostrato".
La cosa utile secondo me, è l'euristica che utilizza per dimostrare automaticamente un teorema, ed è piuttosto potente perchè si può gestire qualunque tipo di induzione e scrivere veri e propri linguaggi (con sintassi, semantica, ecc...) ma formalizzare tutto è umanamente (umano singolo/tempo) impossibile.

Poi è vero che è un bel filone di ricerca, poi per l'utilità ho avuto la tua stessa impressione

"vict85":Intendo dire che se dimostra un teorema prima dell'uomo allora si può usare il risultato (purché la dimostrazione sia corretta)

questo lo fa già con le euristiche, ma per poter fare ciò ad oggi bisogna usare una sintassi complicata e davvero degradante.
Invece tipo Isabelle ha un meta-linguaggio più stile C ma sempre molto complesso.

[vict85]

"Deckard":[quote="vict85"]Crea un nuovo teorema che potrebbe essere usato per dimostrare altro.

Che intendi? Coq non è un programma di dimostrazione automatica, ma, perlopiù, per il checking delle dimostrazioni.[/quote]

Intendo dire che se dimostra un teorema prima dell'uomo allora si può usare il risultato (purché la dimostrazione sia corretta)

[Deckard1]

"vict85":Crea un nuovo teorema che potrebbe essere usato per dimostrare altro.

Che intendi? Coq non è un programma di dimostrazione automatica, ma, perlopiù, per il checking delle dimostrazioni.

[vict85]

"Deckard":[quote="ham_burst"]Se sì, che ne pensate, li ritenete utili?

Dipende cosa intendi per utile. Sono sicuramente un affascinante filone di ricerca, tuttavia allo stato attuale per quanto ne so sono molto lontani da poter essere considerati "utili" nell'accezione comune del termine; nel senso che per formalizzare anche un semplice teorema richiedono davvero molto lavoro. Probabilmente potranno, magari lo sono già, essere utili soprattutto in campi come la teoria dei numeri i cui risultati credo siano relativamente semplici da formalizzare in un sistema formale.
Comunque io sono dell'opinione che la dimostrazione di un teorema sia importante, più che per aver confermato la validità del teorema stesso, per farci comprendere il perché quel teorema è vero. E quindi se coq ci dice che la dimostrazione è esatta, ma noi non siamo in grado di afferrarla, a che serve tutto ciò?[/quote]

Crea un nuovo teorema che potrebbe essere usato per dimostrare altro. In ogni caso per ora i computer non hanno fornito un supporto seziente nelle dimostrazioni quanto più un ausilio al calcolo. Per quanto programmini interessanti da creare e progettare in genere si fermano molto prima di un uomo. Detto questo il computer alle volte trova strade che l'uomo non sempre considera perché l'uomo è più basato sull'esperienza mentre un computer non ha in genere preferenze nette tra metodi diversi.

[Deckard1]

"ham_burst":Se sì, che ne pensate, li ritenete utili?

Dipende cosa intendi per utile. Sono sicuramente un affascinante filone di ricerca, tuttavia allo stato attuale per quanto ne so sono molto lontani da poter essere considerati "utili" nell'accezione comune del termine; nel senso che per formalizzare anche un semplice teorema richiedono davvero molto lavoro. Probabilmente potranno, magari lo sono già, essere utili soprattutto in campi come la teoria dei numeri i cui risultati credo siano relativamente semplici da formalizzare in un sistema formale.
Comunque io sono dell'opinione che la dimostrazione di un teorema sia importante, più che per aver confermato la validità del teorema stesso, per farci comprendere il perché quel teorema è vero. E quindi se coq ci dice che la dimostrazione è esatta, ma noi non siamo in grado di afferrarla, a che serve tutto ciò?