Università degli Studi di Bologna
Facoltà di Scienze Matematiche, Fisiche e Naturali
Corso di Laurea in Informatica
Materia di Tesi: Linguaggi di programmazione
Progettazione e realizzazione con tecnologia XML di basi distribuite
di conoscenza matematica formalizzata
Tesi di Laurea di:
Claudio Sacerdoti Coen
Relatore:
Chiar.mo Prof. Andrea Asperti
Parole chiave: Librerie digitali; Matematica formale; XML; MathML; Proof-assistant
II Sessione
Anno Accademico 1999-2000
A Barbara
e alla mia famiglia
Introduzione
L'eXtensible Markup Language
I Proof-Assistant
Il progetto HELM
Lavori correlati
Organizzazione della tesi
Il proof-assistant Coq
Il Calcolo delle Costruzioni (Co)Induttive
Il Calcolo delle Costruzioni (Co)Induttive in Coq
Il sistema Coq
Esportazione in XML da Coq di oggetti CIC
Una critica all'approccio ``un oggetto, un file''
Il DTD per il livello dei termini e degli oggetti
Il livello delle teorie
L'implementazione del modulo di esportazione
Il modello di distribuzione
Il getter
Un proof-checker per i file CIC della libreria
Progettazione
Implementazione
La presentazione delle prove
L'architettura generale delle trasformazioni presentazionali
Gli stylesheet notazionali
Alcune idee per la resa delle prove
Risultati ottenuti.
Le interfacce utente
I siti di presentazione
L'interfaccia sviluppata in Gtk
Conclusioni
Confronto fra i progetti HELM e MathWeb
Lavori Futuri
Il DTD per il livello dei termini e degli oggetti di CIC
La rappresentazione OCaml dei termini e degli oggetti CIC
Un esempio di file XML per un oggetto CIC
Bibliografia
Ringraziamenti
This document was translated from L
A
T
E
X by
H
E
V
E
A and H
A
C
H
A
.