+ <p>Un dimostratore interattivo e' uno strumento software di
+ ausilio alla dimostrazione formale di teoremi attraverso
+ la collaborazione tra l'uomo e la macchina. Fornisce un liguaggio
+ formale in cui coesistono definizioni matematiche, algoritmi eseguibili,
+ teoremi e relative dimostrazioni, ed un ambiente interattivo che tiene
+ traccia dello stato corrente delle prove, e le aggiorna in funzione dei
+ comandi (tattiche) impartiti dall'utente. </p>
+