EPITA

Introdution à Prolog, cours n° 3

Jean-François Perrot

Le principe de Prolog

But de ce cours

• Objectif

  Tirer au clair les rapports entre Prolog et la théorie logique, en explicitant les termes souvent employés de résolution, d'unification etc.
  
  Le critère opérationnel retenu est celui de la construction progressive d'un modèle réduit de Prolog.
  Au cours de cette progression, on mettra en évidence les différents choix constitutifs de Prolog dans le cadre de la théorie logique  :
  
  • une stratégie de résolution qui exploite la structure des clauses de Horn et des requêtes réduites à des littéraux,
    au risque de boucler...;
  • l'unification sans occur-check, au risque de rencontrer des termes infinis.
    
  
  On aboutira à un "quasi-prolog" présentant le même comportement que le noyau de Prolog à l'exception du cut
  - et bien entendu, avec des temps de calcul radicalement différents.
  Nous ne pouvons pas l'appeler micro-Prolog, car ce nom a été illustré dans la passé par Clark & McCabe.
  

• Organisation

  Cette démarche se fera en deux temps :
  
  
  1. Analyser le processus de résolution dans le cadre propositionnel, qui se prête à une expérimentation aisée.
     On y fait apparaître la stratégie de résolution à la Prolog (variante de la SLD-résolution).
     
     
  2. Passer au 1er ordre, où interviennent l'unification et l'alpha-conversion.
     
     
     
  Chaque étape comprendra deux phases,
  
  
  1. la description des phénomènes
     
     
  2. leur modélisation en Prolog (fichier séparé pour la résolution propositionnelle)