Abstract FR:

Le systeme formel implante s'inspire de la deduction naturelle, s'approchant de l'ecriture des preuves dans un texte mathematique courant. Les resultats prouves peuvent etre sauvegardes et utilises ulterieurement comme regles d'inference pour d'autres preuves