Le but de ce projet est de développer des formalismes logiques permettant de représenter et manipuler des schémas de formules et de preuves en déduction interactive (ou automatique) et d'utiliser ces outils pour aider à la formalisation et à l'analyse de preuves mathématiques (en utilisant des techniques de transformation de preuves par élimination de coupures).