Deep Inference in Matita

La correttezza di una dimostrazione, o di un programma, è spesso diffi- cile da verificare; è normale chiedersi, dopo l'ultimo passaggio: "Ho dimenticato qualche caso?", "I passaggi sono giusti?" o "È questo ciò che volevo dimostrare?". Rispondere a queste domande con certezza è, in generale, impossibile. Ciò che però è possibile, è verificare le dimostrazioni con un formalismo basato su linguaggi funzionali, in grado riconoscere solo dimostrazioni corrette. Questi linguaggi sono alla base dei theorem prover. Ma chi verifica i verificatori? Per non incappare in una regressione infinita, la correttezza dei theorem prover è affidata al criterio di De Bruijn: tutti i calcoli si basano su un ker- nel, il più piccolo possibile. Questo, seppur non garantisce la correttezza, permette di avere sotto controllo il comportamento del verificatore. Inoltre, molti verificatori garantiscono che le formule (anche quelle in- termedie) sono scritte in linguaggi standard (come XML), sì che possano essere lette anche da altri theorem prover. Verificare le dimostrazioni è un obiettivo molto alto e abbiamo voluto ca- pire quanto si possa fare (in termini di semplicità oltre che di completezza) in relazione al calcolo delle strutture. In particolare ci concentriamo sul- l'implementazione di BV, con un proof assistant italiano: Matita. Nel primo capitolo descriviamo il calcolo delle strutture, le sue pecu- liari proprietà, la sintassi, le regole d'equivalenza e quellie di derivazione. Introduciamo, inoltre, il parallelismo tra BVL e CCS. Nel secondo capitolo descriviamo Matita: come è nato, come funziona e, in breve, la sintassi. Cerchiamo di spiegare come può essere usato e quali sono le tattiche principali, focalizzandoci in particolare su quelle che ab- biamo utilizzato per il nostro lavoro. Nel terzo capitolo descriviamo i nostri risultati; dopo aver ulteriormen- te approfondito la relazione tra dimostrazioni con Matita e dimostrazioni con la matita, mostriamo le proprietà che siamo riusciti a dimostrare. Met- tiamo inoltre in evidenza le proprietà che non siamo riusciti ad ottenere, probabilmente per un'implementazione incompleta. Nelle conclusioni chiariamo la scelta di Matita rispetto ad altri possibili theorem prover; inoltre cerchiamo di dare uno spunto per il miglioramento dell'implementazione attuale.