386 B
386 B
Démonstrateur automatique en Caml
Implémenté avec amour en Caml.
Je ne sais absolument plus l'utiliser (ça date de 2013) alors si quelqu'un sait, je l'autorise à s'acheter un Carambar.
Utilise le [système de Gentzen de calcul de séquent] (http://www.pps.univ-paris-diderot.fr/~kesner/enseignement/licence/logique/Gentzen-predicats-4.pdf).
Joie et bonheur sur vos familles.