Metodi formali per la pratica matematica

La comparsa e la rapida evoluzione dei software di dimostrazione interattiva aprono nuovi scenari nell'impiego, nello sviluppo e nella comunicazione della Matematica. Nella prima parte del seminario si cercherà di fornire un'introduzione generale all'argomento e di dare conto dello stato dell'arte di questa disciplina emergente. Nella seconda parte verrà presentato uno sviluppo dell'analisi quaternionica con il sistema di dimostrazione interattiva HOL Light.