Travaux Pratiques

À la fin de chaque TP, envoyez votre compte rendu par email à votre enseignant

Utilisez la commande :

mailx -s "[TPINF124] TP n : nom1 & nom2"   email de l'enseignant   <   fichier.c

n désigne le numéro du TP et nom1, nom2 sont les noms de famille du binôme.

Transfert des fichiers de windows à unix

  1. Téléchargez les fichiers depuis le site web et sauvez les sous windows
  2. Utilisez le logiciel winSCP qui permet de faire glisser des fichiers de windows vers votre compte unix

    XSG est disponible sur le bureau et se lance en donnant :

    hôte: gallien
    utilisateur: votre login_ujf    mot de passe

Compilation C sans warning : utilisez la commande gcc -lm -w -o run main.c

Travaux pratiques à réaliser en C

Travaux pratiques à réaliser en Ocaml

  • Le fichier des règles du prouveur: regles.ml
    1. Compilation du prouveur
      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.
    2. Chargement du prouveur dans l'interprète ocaml
      utilisez la commande ocaml prouveur.cmo
      ou bien ocaml puis #load "prouveur.cmo";; dans l'interprète
    3. Preuves en déduction naturelle

      • 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
Responsables de l'UE : Cristian Éné & Michaël PÉRIN