1. créez un répertoire inf124/ocaml/
2. copiez le fichier prouveur.tgz dans inf124/ocaml/
3. décompresser le fichier prouveur.tgz avec la commande tar -xf prouveur.tgz
4. dans le répertoire prouveur/src/, exécutez la commande chmod u+x makeit ; ./makeit
5. vérifiez que vous avez bien les fichiers prouveur.cmo et prouveur.cmi dans le répertoire inf124/ocaml/prouveur/
6. copiez les 4 séries d'exercices dans le répertoire inf124/ocaml/prouveur/ et faîtes les.

utilisez la commande ocaml prouveur.cmo
ou bien ocaml puis #load "prouveur.cmo";; dans l'interprète

• objectif des TP
  Construire des arbres de preuves en ocaml: exo_1_1.html
  Traduire les arbres de preuve sous forme textuelle.
• TP 7 - Familiarisation avec le prouveur
  1. Exemple introductif: serie1.sql.ml
  2. Preuve propositionnelle: serie2.sql.ml
• TP 8 - Preuve utilisant les définitions
  1. de la théorie des ensembles: serie3.sql.ml
  2. de la théorie des relations: serie4.sql.ml
• PROJET 2 - traduction des arbres de preuves en preuve textuelle
• TP 10 - soutenance du projet 2