LEGO (logiciel)

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
image illustrant les logiciels image illustrant les mathématiques
Cet article est une ébauche concernant les logiciels et les mathématiques.

Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

Page d'aide sur l'homonymie Pour les articles homonymes, voir Lego (homonymie).

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]