Assistente di prova solo per matematica

Question

La maggior parte degli assistenti di prova sono linguaggi di programmazione funzionale con tipi dipendenti. Possono provare programmi/algoritmi. Mi interessa, invece, l'assistente di prova adatto al meglio per la matematica e solo (calcolo per esempio). Puoi consigliarne uno? Ho sentito parlare di Mizar ma non mi piace che il codice sorgente sia chiuso, ma se è meglio per la matematica lo userò. Quanto bene i nuovi linguaggi come Agda e Idris sono adatti per prove matematiche?

Answer 1

Coq dispone di ampie librerie che coprono l'analisi reale. Vari sviluppi vengono in mente:

• il standard library e progetti di costruzione su di esso, come il progetto ormai defunta coqtail [1] (con ampia copertura delle serie di potenze e di un po 'di lavoro sui numeri complessi) o il più recente coquelicot. Tutti questi si basano su una definizione assiomatica dei reali presented here.

• Un approccio più costruttivo viene fornito dal progetto the C-CoRN che inizia con la creazione effettiva dei valori reali.

Un altro modo per affrontare i reali è passare a un'analisi non standard. Questo è ciò che le persone che usano ACL2 hanno fatto.

Per una visione più generale del campo, è consigliabile leggere this survey paper dalle persone coinvolte nel progetto coquelicot.

[1] completa divulgazione: sono stato coinvolto in quel progetto