La méthode des arbres en Ocaml

La méthode des arbres¹ permet de démontrer qu'une formule est ou non un théorème de la logique.

Marin vient de publier son premier code sur Github. Il s'agit d'un programme en Ocaml qui engendre le code graphviz pour dessiner la preuve.

C'est le projet treeproof.