export PATH=/afs/math.unifi.it/service/types/Programs/bin:/srv/BLCR/bin:$PATH export LD_LIBRARY_PATH=/srv/BLCR/lib:$LD_LIBRARY_PATH
Documentazione di HOL Light
Tutorial (Essenziale per seguire il corso, meglio stamparselo)
Guida Rapida (I teoremi e i comandi più usati in HOL Light; molto utile)
Emacs
Reference Card (I comandi più importanti in un solo foglio)
EmacsWiki (Tutto quello che volete sapere su Emacs)
Esercizi (Per accompagnare la lettura del tutorial)
A Special Issue on Formal Proof, Notices of the AMS, Dicembre 2008
Thomas Hales, Formal Proof—Theory and Practice
Georges Gonthier, Formal Proof—The Four-Color Theorem
John Harrison, Formal Proof—Theory and Practice
Freek Wiedijk, Formal Proof—Getting Started
Marco Maggesi, Carlos Simpson, Verifica automatica del ragionamento matematico. Bollettino U.M.I., Sezione A, La Matematica nella Società e nella Cultura, Serie VIII, Vol. IX-A, Dicembre 2006/1, 361-389
Un esempio di formalizzazione (sviluppata nel corso di Seminario di Geometria dell’anno accademico 2008-2009) sulle basi di una topologia.
Un esempio di formalizzazione di un linguaggio di processo (Geometria Computazionale Simbolica, A.A. 2009-2010).
Per installare HOL Light su di una macchina Debian o Ubuntu seguire queste istruzioni.
Aggiungere questa riga al file ~/.bashrc
export PATH=/afs/math.unifi.it/service/types/Programs/bin:/srv/BLCR/bin:$PATH export LD_LIBRARY_PATH=/srv/BLCR/lib:$LD_LIBRARY_PATH
Aggiungere queste righe al file ~/.emacs
(add-to-list 'load-path "/afs/math.unifi.it/service/types/Sources/hol-light-mode")
(autoload 'hol-light-mode "hol-light-mode" nil t)
(setq auto-mode-alist (cons '("\\.ml$" . hol-light-mode) auto-mode-alist))
C = orario attuale del corso
| Lu | Ma | Me | Gi | Ve | |
|---|---|---|---|---|---|
8.30 |
|||||
9.30 |
|||||
10.30 |
|||||
11.30 |
|||||
12.30 |
C |
||||
13.30 |
[C] |
||||
14.30 |
C |
||||
15.30 |
C |
C |
|||
16.30 |
C |
||||
17.30 |
