LEGO (logiciel)

LEGO, est un assistant de preuve interactif, créé par Randy Pollack en 1994

Il possède plusieurs systèmes de types :

  • le Logical Framework d'Edimbourg
  • le calcul des constructions
  • le calcul des constructions généralisé
  • la théorie unifiée des types dépendants
[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[Quoi ?].

Liens externes

  • icône décorative Portail des mathématiques
  • icône décorative Portail de la logique
Cet article est issu de Wikipédia. Sauf mention contraire, le texte est disponible sous Creative Commons Attribution-Share Alike 4.0. Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.