À 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

où 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

• Bibliothèques à récupèrer : hasard.c, basic.c, bool.c, colors.c, quantificateur.c
• Relations binaires
  • Fichier principal main.sql.c
  • Séance 1 - TP1 - composition de relations
    • objectif du TP1
      1. exemple de trace d'exécution: trace.txt
      2. exemple de graphe de relations obtenu avec graphviz:
         est_moitie_de.pdf, est_diviseur_non_trivial_de.pdf
    • le semi-anneau des booléens: boolean_semi_ring.sql.c
    • affichage de relations: relation_affichage.sql.c
    • construction de relations: relation_construction.sql.c
    • opérations sur les relations: relation_operation.sql.c
    • main du TP1: tp1.sql.c
  • Séance 2 - TP2 - cloture transitive et calcul du plus court chemin
    • objectif du TP2
      Exemples de relations Distance entre villes et les relations Mappy correspondantes obtenues par cloture reflexive-transitive:
      1. Distance .pdf, Mappy.pdf, Distance + Mappy .html
      2. Distance .pdf, Mappy .pdf Distance + Mappy .html
    • le semi-anneau mappy: mappy_semi_ring.sql.c
    • relation reflexive: relation_reflexive.sql.c
    • relation symétrique: relation_symetrique.sql.c
    • cloture transitive d'une relation: relation_cloture.sql.c
    • affichage de relations: relation_affichage.sql.c
    • création d'une relation: relation_au_hasard.sql.c
    • main du TP2: tp2.sql.c
  • Séance 3 - TP3 - relations et fonctions
    • objectif du TP3
      Énumérer les relations reflexives, symétriques, anti-symétrique, transitives
      celles qui sont des relations d'ordre, d'équivalence
      celles qui sont des fonctions injectives, surjectives, bijectives
    • relation anti-symétrique: relation_anti_symetrique.sql.c
    • énumération de relation: relation_enumeration.c
    • relation fonction: relation_fonction.sql.c
    • main du TP3: tp3.sql.c
  • Séance 4 - PROJET 1 - relation d'ordre et optimisation d'exécution
  • Séance 5 - soutenance du projet 1
  • TP optionnel : si vous avez tout fini en avance - classes d'équivalence et réseaux sociaux
    • objectif du TP4
      Identification automatique des groupes sociaux dans un réseau social de type Facebook
      Le réseau d'amis est vu comme une relation qu'on transforme en relation d'équivalence
      Les groupes sont alors les classes d'équivalence de la relation (aussi appelées composantes fortement connexes du réseau).
    Exemples
    1. Réseau social .pdf, Réseau + Groupes .pdf
    2. Réseau social .pdf, Réseau + Groupes .pdf
    • relation d'équivalence: relation_equivalence.sql.c
    • main du TP4: tp4.sql.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