LEGO (logiciel)
Apparence
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 mathématiques informelles[Quoi ?].
Liens externes
[modifier | modifier le code]- (en) Site officiel