2 - Programmation Logique.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Programmation Logique\n",
    "\n",
    "La programmation impérative a un défaut majeur : elle mélange le \"quoi\" (la tache qu'on souhaite résoudre) et le \"comment\" (la procédure à suivre pour résoudre la tâche). En programmation logique, on spécifie le problème à résoudre de manière **déclarative** et c'est le **moteur d'inférence du langage** qui trouve la/les solutions au moyen d'un algorithme de résolution. \n",
    "\n",
    "Au lieu de voir un programme comme une suite d'instructions, la programmation logique définit un programme comme une théorie logique à laquelle on soumet des théorèmes que l'on souhaite verifier. Un programme est ainsi une suite d'axiomes que la machine doit combiner pour établir les conditions sous lesquelle une assertion donnée est vraie.\n",
    "\n",
    "**Prolog :** 1er langage de programmation logique complet, inventé par Colmerauer et Roussel dans les années 1970.\n",
    "\n",
    "A son apogée dans les années 80, la programmation logique a été considérée comme la brique première de l'**Intelligence Artifielle Générale**, fournissant un paradigme dans lequel on alimente une **base de connaissances** en perpetuelle croissance, permettant à la machine d'effectuer des raisonnements de plus en plus complexes. Les plus optimistes y voyaient une procédure systématique conduisant in fine à égaler l'intelligence humaine.\n",
    "\n",
    "https://book.simply-logical.space/\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Logique clausale\n",
    "\n",
    "En programmation logique, un programme est un ensemble de **clauses**. \n",
    "Une clause est une **disjonction** (ou une conjonction) de **literaux**.\n",
    "Un **literal** est un **atome** ou sa **négation**.\n",
    "\n",
    "> Exemple : $A \\lor \\lnot B \\lor C \\lor \\lnot D$\n",
    "\n",
    "* Une clause comportant uniquement des **literaux positifs** est un **fait**\n",
    "* Une clause comportant uniquement des **literaux negatifs** est un **but** (ou une **requète**)\n",
    "* Sinon la clause est une **règle**\n",
    "\n",
    "En programmation logique, on écrit \n",
    "````prolog\n",
    "B.             # Un fait (fact)\n",
    "A;C :- B,D.    # Une règle (rule)\n",
    ":- C           # Une requète (query)\n",
    "````\n",
    "\n",
    "Pour exprimer $A \\lor C \\lor \\lnot B \\lor \\lnot D$ que l'on peut aussi ecrire \n",
    "\n",
    "$$B \\lor D \\Rightarrow A \\land C$$\n",
    "\n",
    "On lit \"B est vrai ou D est vrai **si** A et B sont vrais\"\n",
    "\n",
    "Un programme complet est la conjonction de toutes ses clauses\n",
    "\n",
    "# Logique clausale propositionnelle (ordre 0)\n",
    "\n",
    "En logique propositionnelle tous les atomes sont des propositions.\n",
    "**Proposition :** une assertion qui est soit vraie, soit fausse\n",
    "Exemples :\n",
    "* \"Le cours a commencé\"\n",
    "* \"Le cours ne se terminera pas\"\n",
    "\n",
    "# Logique clausale relationnelle \n",
    "\n",
    "La logique clausale relationnelle étend la logique propositionnelle en permettant de définir des règles qui s'appliquent identiquement à plusieurs entités arbitraires, remplaçant potentiellement une infinité de règles propositionnelles. Pour cela, elle définit la notion de **prédicat**. Un predicat est un atome s'appliquant à une ou plusieurs **variables**. On note $p(X)$, où X peut prendre n'importe quelle valeur de l'univers considéré.\n",
    "\n",
    "On peut alors exprimer des théories telles que \n",
    "\n",
    "* \"Tous les hommes sont mortels\" (règle) :  `mortel(X) :- homme(X)`\n",
    "* \"Socrate est un homme\" (fait) : `homme(socrate)`\n",
    "* \"Socrate est il mortel ?\" (requete) : `:- mortel(socrate)`\n",
    "\n",
    "Convention : en Prolog, on note les variables en majuscules, les constantes en minuscule\n",
    "\n",
    "# Logique des prédicats (1er ordre)\n",
    "\n",
    "En logique relationnelle, on ne peut pas exprimer la clause \"Everybody needs somebody to love\". \n",
    "\n",
    "> Question : Que manque-t-il à la logique relationnelle pour exprimer ce type de clause ?\n",
    "\n",
    "La logique clausale des prédicats ajoute la notion de **terme**. Un terme peut être\n",
    "* Simple : une constante $c$ ou une variable $X$\n",
    "* Composé : un foncteur $f(A,b,g(c),\\dots)$ ou A,b,g(c),etc sont des termes (simples ou eux-mêmes composés)\n",
    "\n",
    "Un foncteur est syntaxiquement identique à une fonction (c'est un object mathématique qui accepte des arguments) mais sémantiquement différent : un foncteur n'associe pas de valeur particulière à ses arguments, on ne l'évalue jamais. On se contente de l'**unifier**. L'unification consiste à remplacer les variables par une valeur possible, par exemple $chien(jean)$ et garder le résultat tel quel. On ne saura jamais comment s'appelle le chien de Jean, mais on peut l'utiliser en tant que tel et l'identifier aux autres apparitions de $chien(jean)$.\n",
    "\n",
    "Exemple :\n",
    "````\n",
    "aime(X,cheri(X)). # Fait : \"tout le monde aime quelqu'un\"\n",
    "````\n",
    "\n",
    "La logique clausale des prédicats est sémantiquement équivalente à la logique \"classique\" des prédicats, qui utilise un syntaxe plus riche (quantificateurs $\\forall$ et $\\exists$:\n",
    "* Toute clause est trivialement convertie en forme normale conjonctive (CNF = conjonction de disjonction de literaux) et inversement\n",
    "* Toute formule de la logique des prédicats peut être convertie en CNF également et reciproquement (par Skolemisation)\n",
    "\n",
    "Conséquence : la programmation logique permet de contruire des théories sur des univers infinis, tels que l'ensemble des entiers\n",
    "\n",
    "# Logiques d'ordre supérieur ...\n",
    "\n",
    "En logique des prédicats, les foncteurs sont des constantes. On ne peut donc pas exprimer des règles telles que \n",
    "\n",
    "$$ \\forall P : symmetric(P) \\Leftrightarrow \\forall X,Y, P(X,Y) \\Rightarrow P(Y,X) $$\n",
    "\n",
    "En Prolog \"classique\", on s'arrête à la logique des prédicats (ordre 1)\n",
    "\n",
    "\n",
    "# Resolution\n",
    "\n",
    "La résolution d'une requête est effectuée automatiquement par le moteur d'inférence, en combinant deux procédures : l'unification et la réfutation.\n",
    "La preuve par réfutation consiste à supposer pour chaque valeur des variables de la requete que la proposition à démontrer est fausse, puis parcourir les règles jusqu'à établir une contradiction. \n",
    "\n",
    "La méthode par réfutation est une recherche arborescente, particulièrement efficace car elle evite de verifier exhaustivement toutes les règles : on s'arrête dès qu'une contradiction est trouvée. Dans le cas de la logique propositionnelle, la complexité de l'algorithme de refutation est polynomiale.\n",
    "\n",
    "On a alors prouvé que sous la théorie définie la requête est vraie pour cette valeur. \n",
    "NOTE : En raison du \"problème du monde clos\", on ne peut seulement prouver qu'un proposition est vraie, jamais qu'une proposition est fausse. En effet, la théorie donnée ne permet jamais de savoir si la proposition est réellement fausse, ou si la théorie n'est pas assez riche. Sous l'hypothèse du monde clos, on suppose que tout ce qui est vrai peut l'être démontré, mais cela implique que ce qui n'a pas pu être démontré sous les axiomes donnés est forcément faux.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# TP\n",
    "\n",
    "Rendez-vous sur https://swish.swi-prolog.org/p/jfellus-diu-eil-ia.swinb"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Voir aussi\n",
    "\n",
    "https://www.enib.fr/~tisseau/pdf/course/td-prolog.pdf\n",
    "\n",
    "https://github.com/yuce/pyswip/blob/master/examples/sudoku/sudoku.pl"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.7.8"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}