LEGO (logiciel)
LEGO, est un assistant de preuve interactif, créé par Randy Pollack en 1994
Il possède plusieurs systèmes de types :
[Quoi ?]
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.
Liens externes
- (en) Site officiel
Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.