Zenon Modulo

Notoriété 25 %

Zenon Modulo est un solveur de preuves automatisé pour la logique du premier ordre classique avec types polymorphes. Il accepte les fichiers d'entrée avec la syntaxe TPTP (FOF et TFF1) et Dedukti. Il peut produire des certificats de preuve pour Dedukti. Il est utilisé dans les projets FoCaLiZe et BWare.

Dépôt de code

https://github.com/Deducteam/zenon_modulo (nouvelle fenêtre)19 étoiles

Cas d'utilisation métiers

Intégration avec les outils de preuve formelle FoCaLiZe et BWare
Preuve automatisée de théorèmes pour la logique du premier ordre classique avec types polymorphes

Cas d'utilisation fonctionnel

Utilise de l'intelligence artificielle

Organisation

Administration centrale
- Gouvernement (Premier ministre et ministères)
  - Ministère de l’Enseignement supérieur, de la Recherche et de l'Espace
    - Établissements d'enseignement supérieur et de recherche - Ministère chargé de l'Enseignement supérieur
      - École normale supérieure Paris-Saclay (organisation rattachée)

Outils utilisés

OCaml
ImageMagick

Description générée le mardi 19 mars 2024 à 15:50:42

D'autres initiatives de la même organisation

lambdapi
github.com/Deducteam/lambdapi
Logipedia
github.com/Deducteam/Logipedia
Agda2Dedukti
github.com/Deducteam/Agda2Dedukti
CoqInE
github.com/Deducteam/CoqInE