Projet : réalisation d'un système déductif
Le projet INF121 présente deux notions essentielles en informatique :
  • les relations étudiées en MAT112 et INF122 : voir « Langage mathématique ».
  • L'algorithme d'unification que l'on retrouve dans de nombreux problèmes informatiques. Par exemples,

    1. la construction match d'ocaml est un cas d'unification simplifiée
    2. le typage d'ocaml utilise l'unification
    3. la vérification de l'application des règles de déduction (en INF122) utilise l'unification
    4. la recheche des fichiers dont les noms correspondent à "INF***-DM.***" est un problème d'unification

Le projet fait travailler sur les séquences, les séquences de séquences, les séquences de séquences de couples de séquences, etc... C'est un bon entraînement pour l'examen.

Le projet présente une application réelle et puissante de l'informatique : les systèmes de déduction automatique.

Les étudiants qui veulent prouver leur talent de programmeur ocaml trouveront en bas de page une suggestion d'extension qui leur demandera de la réflexion.

Le projet comporte 8 parties et deux illustrations qui sont données sous forme de squelettes caml à compléter. Le squelette correspondant à une partie est accessible ci-dessous par le lien dans le titre de la partie.

Qu'est-ce qu'un système déductif ?

Un système déductif est constitué de règles de déductions (les
règles) et de connaissances initiales (les faits).

Le système utilise les règles pour faire des déductions à partir des
connaissance initiales. Il obtient alors de nouvelles connaissances et
peu recommencer à appliquer les règles. Il produit ainsi toutes les
déductions possibles. 

Ces systèmes (appelés systèmes experts) servent à automatiser et
accélérer le raisonnement. Ils sont utilisés dans de nombreux
domaines:

- En médecine, pour aider à faire un diagnostique : le médecin entre
  les symptômes du patient et le système lui fournit la liste des
  causes possibles.

- En électronique, mécanique, électricité : pour aider les réparateurs
  à trouver la cause d'une panne à partir des symptômes. On parle de
  système d'aide au diagnostique de pannes. C'est ce qu'utilisent les 
  garagistes quand ils branchent un ordinateur sur les voitures récentes.

- En criminologie pour traquer les tueurs en série et faire le lien
  entre divers crimes qui comportent des similitudes. Il s'agit
  d'établir le profil des criminels à partir du mode opératoire du
  crime. On parle de système de profilage (profiling en anglais).

- En marketing sur les sites de vente par internet, pour déterminer le
  profil d'un client à partir de ses achats et ainsi lui proposer des
  offres promotionnels qui correspondent à ses goûts. C'est aussi un
  système de profilage.

Certains journaux de vulgarisation scientifique emploient le terme de
systèmes intelligents ou d'intelligence artificielle à propos des
systèmes experts. Le terme «intelligent» est tout à fait inapproprié ;
il n'y a rien d'intelligent dans ces systèmes, ils sont pûremenent
algorithmiques : c'est à dire mécaniques, méthodiques et systématiques.

La puissance de ces systèmes provient du fait qu'ils ne font pas
d'erreur de raisonnement et qu'ils considèrent toutes les déductions
possibles (alors que les humains peuvent oublier des cas si le
problème devient trop complexe).

En revanche, les déductions des systèmes experts se basent sur des
règles de déduction qui sont donnés par des experts humains. C'est là
que se cache toute l'intelligence : si une règle est erronée alors le
système fait des déductions erronées... 

Un exemple de système déductif

Les connaissances initiales sont appelées des faits. Elles sont représentées
par des relations à un ou plusieurs arguments.

Exemples: - pere(Jean, Alain) est une relation «pere» à deux arguments qui modélise le fait que Jean est le père d'Alain - petit(Jean) est une relation «petit» à un argument qui modélise le fait que Jean est petit.
Les règles de déduction génèrent de nouveaux faits à partir des faits déjà connus.
Exemples: - pere(x,y), petit(x) --> petit(y) Cette règle modélise la déduction suivante : « si le père de y est petit alors y est petit » - pere(x,y), pere(x,z) --> frere(y,z) Cette règle modélise la déduction suivante : « si x est le père de y et de z alors y et z sont frères »
Exercice : Donnez la règle qui génère la relation « cousin » à deux arguments à partir des relations père et frère. Déductions : si on lance le système expert avec ces deux règles sur les faits précédents, on obtient toutes les déductions possibles suivantes : pere(Jean,Alain), petit(Jean), petit(Alain) Si on ajoute un nouveau fait : pere(Jean,Paul), le système ajoute les nouveaux faits déduits : frere(Paul,Alain), frere(Alain,Paul), petit(Paul) mais aussi frere(Alain,Alain), frere(Paul,Paul)

Utilisation d'un système déductif

  1. Comment charger la bibliothèque Inf121 ? <-- mis à jour le 06/04/2011

    c'est expliqué dans l'onglet outils du site

  2. SystemeD.cmo, SystemeD.cmi <-- mis à jour le 30/03/2011

    Tapez   ocaml -version   pour connaître la version d'ocaml que vous utilisez
    puis téléchargez les fichiers correspondant à votre version.

  3. Chargez le module SystemeD dans l'interpréteur Ocaml à l'aide des commandes :
        #load "SystemeD.cmo" ;;
        include SystemeD ;;
       
  4. Téléchargez l'un des exemples de règles suivants, lisez le et répondez aux questions:

    • déduction de relations de parenté : exemple1.ml
    • inférence de type : exemple2.ml <-- ajouté le 30/03/2011
  5. Concevez un système de règles pour l'un des domaines cités en introduction qui vous servira d'exemple pour votre démonstration de fin de projet.

    • domaine médical :
      souffre(x,maladie) /\ contagieux(maladie) /\ proche(x,y) ---> souffre(y,maladie)
      
      resistant(x,maladie) /\ parent(x,y) ---> resistant(y,maladie)
          
      mal(x,Gorge) /\ symptome(x,Fievre) --> souffre(x,Angine)
      
    • domaine informatique : typage
      expr(e,op,x,y) se lit « l'expression e vaut x op y »
      
      type(x,t1) /\ type(x,t2) /\ t1=/=t2 --> conflit(x,t1,t2)
      
      expr(e,f,a1,a2)  /\ type(f,t1,t2,tres) --> type(e,tres), type(a1,t1), type(a2,t2)
      
      type(+,Int,Int,Int)  
      
      type(=,t,t,Bool)
      
      expr(e,=,x,y) /\ type(x,t) ---> type(y,t)
      
      expr(e,=,x,y) /\ type(y,t) ---> type(x,t)
      
    • domaine mathématique et logique (lien avec MAT112 et INF122) :
      relations d'équivalence, relations d'ordre
      Donnez la règle qui traduit le fait qu'une relation binaire R est :
      • transitive : R(x,y) /\ ........ ---> R(x,z)
      • reflexive
      • symétrique
      • anti-symétrique : .......... /\ .......... ---> Eg(x,y)

      1. Utilisez ces règles pour construire la plus petite relation Ro qui contient Ro(a,d), Ro(a,e), Ro(d,b), Ro(c,b) et qui est une relation d'ordre
      2. Utilisez ces règles pour construire la plus petite relation Re qui contient Re(a,d), Re(a,e), Re(d,b), Re(c,b) et qui est une relation d'équivalence
    • domaine criminel :
      meurtre(x,arme) /\ possede(y,arme) --> suspect_meutre(y,x)
      
    • domaine de la géométrie euclidienne :
      perpendiculaire(d1,d2) /\ perpendiculaire(d2,d3) --> parallele(d1,d3)
      
    • domaine commercial :
      achat(x,marchandise) /\ aime(individu,marchandise) --> habite_chez(individu,x)
      

    • ou tout autre domaine de votre choix qui pourrait se prêter à des déductions automatiques

Réalisation d'un système déductif

Le but du projet est de réaliser un système déductif capable de calculer toutes les déductions que l'on peut obtenir à partir de faits et de règles de déductions.

Représentation et affichage des données

Conventions de représentation

 - les noms des relations  sont représentés par des chaînes de caractères, 

 - les noms de  variables  sont représentés par des chaînes de caractères 
   commençant par une minuscule

 - les noms de  constantes sont représentés par des chaînes de caractères 
   commençant par une majuscule

 - les relations sont représentées par un couple (nom de la relation, séquences des variables)
     
 - les règles sont représentées par un couple de séquences de relations :
    (les relations à gauche du symbole "-->" , les relations à  droite du symbole "-->")  

Représentation des données (partie0.ml)

Représentation des faits

Une relation est un couple (nom, liste des arguments)

 type relation = string * string list

Les arguments sont des noms :
 - les constantes commencent par une Majuscule comme Jean, Alain, Paul, A, B, C 
 - les variables  commencent par une minuscule comme x, y, z, le_pere_de_x 

Exemples :

 - La relation  pere(Jean,Alain)  est représenté par le couple ("pere",["Jean";"Alain"])

 - ("frere",["Paul";"Alain"])  est un fait   
    
   car les arguments sont des constantes (débutent par une majuscule)

 - ("frere",["x1";"x2"])       est un motif 
 
   car les arguments sont des variables  (débutent par une minuscule) 

Représentation des règles

Une règle est un couple de listes de relations 

 type regle = relation list * relation list

              les prémisses   les conclusions (il peut y en avoir plusieurs)

Exemples :

 - La règle « pere(x,y), petit(x) --> petit(y) » est représentée par le couple

   ( [ ("pere",["x";"y"]) ; ("petit",["x"]) ] , [ ("petit",["y"])] )

Exercice :

 Donnez la représentation de la règle qui génère la relation « frere »

Constructeurs, sélecteurs et prédicats sur les relations (partie1.ml)

Mise en page et affichage des faits et des règles (partie2.ml)

Manipulations des faits (partie3.ml)

 Ajout, Retrait d'un fait, Élimination des faits redondants

Sélection des faits et des règles à afficher (partie4.ml)

Application d'une règle de déduction

Principe


1. On utilise le principe d'unification ci-dessous 
   pour savoir si une règle peut s'appliquer et 
   trouvez la valeur des variables des motifs de la règle

puis

2. on utilise le principe de substitution ci-dessous 
   pour calculer les connaissances qu'ajoute 
   l'application de la règle

Substitution et unification (partie5.ml <-- /!\ modifiée le 30/03/2011)

1. Substitution: définition et principe de substitution

Une substitution est une séquence de couple (variable, valeur) qui
indique par quelle valeur on doit remplacer la variable.

Écrire une fonction est_substitution qui prend en paramètre une
liste de couples (variable, constante) et répond faux si une même
variable apparaît dans plusieurs couples avec des constantes
différents et répond vrai sinon.

Exemples :

 est_substitution([("x","Jean") ; ("y","Alain")]) répond vrai

 est_substitution([("x","Jean") ; ("y","Alain") ; ("x","Jean") ]) répond vrai

 est_substitution([("x","Jean") ; ("x","Alain") ]) répond faux


Exercice :

 que doit répondre  est_substitution([]) ?


Écrire une fonction simplifie_substitution qui prend en
paramètre une liste de couples (variable, constante) pour laquelle
est_substitution répond vrai et qui retourne la substitution dans
laquelle on a éliminé les couples redondants.


Exemple :

 simplifie_substitution([("x","Jean") ; ("y","Alain") ; ("x","Jean") ]) 

 retourne [("x","Jean") ; ("y","Alain")]


Exercice :

 que doit répondre simplifie_substitution([]) ?

 que doit répondre simplifie_substitution([("x","Jean") ; ("x","Alain") ]) ?
 Application d'une règle par subsiSélection des faits et règles à afficher

2. Unification : définition et principe d'unification

On dit que le fait pere(Jean,Alain) et le motif pere(x,y) s'unifient,

c'est à dire qu'ils sont égaux si on remplace (on dit substituer) x par Jean et y par Alain. 

Définition 
On dit que la liste [("x","Jean") ; ("y","Alain")] est la substitution
qui permet d'unifier le fait et le motif.


Par contre, 

- le fait pere(Jean,Alain) et le motif frere(x,y) ne s'unifient pas.
  Il est impossible de les rendre égaux peu importe ce qu'on choisit pour x et y.

- le fait pere(Jean,Alain) et le motif pere(x,x) ne s'unifient pas.
  car il faudrait prendre x=Jean et x=Alain ce qui est contradictoire.


On vous demande de réaliser une fonction unification qui prend en paramètre un fait et un motif
et qui retourne

- soit faux et la liste vide si le fait et le motif ne peuvent pas s'unifier

- soit vrai et la substitution des variables qui permet d'unifier le fait et le motif 


Exemples :

 - unification( ("pere",["Jean","Alain"]) , ("pere",["x","y"]) ) doit retourner

   (vrai,[("x","Jean") ; ("y","Alain")])

 
 - unification( ("pere",["Jean","Alain"]) , ("frere",["x","y"]) ) doit retourner

   (faux,[("x","Jean") ; ("y","Alain")])

Énumération (partie6.ml)

Cette partie vous amènera à écrire des fonctions qui construisent les vecteurs d'un produit d'ensembles. Ces fonctions seront utilisées dans la partie 7 pour énumèrer tous les candidats qui sont susceptibles de s'unifier avec la prémisse d'une règle.

Déduction (partie7.ml)

Cette partie vous amènera à écrire une fonction qui prend en paramètre
  - une règle 
  - des faits 
 
  • Elle regroupe, sélectionne, et énumère grâce aux fonctions de la partie 6, tous les candidats parmi les faits sur lesquelle la règle est susceptible de s'appliquer.
  • L'unification de la prémisse de la règle avec ces candidats indique si la règle peut effectivement s'appliquer et produire de nouveaux faits. On réutilise la fonction de la partie 5 qui applique une règle à chaque candidat.
  • Finalement, la fonction retourne les nouveaux faits produits en appliquant la règle à tous les candidats.

Saturation (partie8.ml)

Cette partie est fournie par les enseignants.
  • Elle utilise la fonction de déduction de la partie 7 pour saturer l'ensemble des faits, c'est-à-dire produire tous les faits possibles en appliquant toutes les règles à tous les candidats possibles jusqu'à ce qu'on ne puisse plus produire de nouveaux faits.
  • On dit alors que l'ensemble des faits est stable pour les règles de déduction.
  • On a ainsi déduit tout ce qu'il était possible de déduire des faits initiaux.
  • L'intérêt du système de déduction est que l'on est certain de n'avoir oublié aucune des déductions possibles.

Extension

Cette partie est destinée aux étudiants qui ont fini en avance les parties précédentes. Les fonctions à réaliser ne sont pas spécifiées. Cette partie demande donc plus de réflexion.

Définitions de règles avec condition d'application

Vous avez remarqué que la règle :
 père(x,y), père(x,z) ---> frère(x,y)
produit le fait : frère(Jean,Jean) à partir de père(Paul,Jean)

Pour éviter de produire cette déduction inintéressante on aimerait préciser que y et z doivent être différents. On souhaite donc modifier le système de déduction pour qu'il soit capable d'utiliser des règles avec des conditions de la forme y<>z ou y=z.

Par exemple :

 père(x,y), père(x,z) ---> frère(x,y)  si  y<>z
Imaginez les modifications à apporter aux parties 1 à 8 afin de traiter les règles avec conditions ; demandez conseil à votre tuteur.
Responsables INF121 : Michaël PÉRIN, François PUITG