LEGO, est un assistant de preuve interactif, créé par Randy Pollack en 1994
Il possède plusieurs systèmes de types :
Les preuves sont développées dans le style de la déduction naturelle. La synthèse d'argument et le polymorphisme permettent de rendre la formalisation proche des .
Liens externes
Catégorie:Assistant de preuve