MOLOG

Au milieu des années 1980, le langage PROLOG est devenu une référence en matière de langage de programmation permettant d'utiliser l'expressivité de la logique mathématique en lieu et place de l'enchainement d'instructions ou de fonctions caractéristiques des langages impératifs ou fonctionnels. L'un des problèmes de PROLOG était sa limitation à l'utilisation des clauses de Horn en calcul des prédicats du premier ordre. Plusieurs équipes se sont lancées dans la réalisation de méta-interpréteurs spécifiques, généralement écrits eux-mêmes en PROLOG, mais qui permettaient d'étendre PROLOG à d'autres logiques, comme Templog[4] ou Temporal Prolog[5] pour la logique temporelle, N-Prolog[6] pour les logiques hypothétiques, ou les extensions de contexte[7].

Le premier but de MOLOG était d'être capable de traiter de façon générique toutes les formes de logique, contrairement aux méta-interpréteurs spécialisés sus-cités. Pour ce faire, le système se décomposait en trois parties (au lieu de deux pour un système PROLOG classique):

• Le moteur d'inférence
• Les règles de résolution
• La base de clauses

Le moteur d'inférence et la base de clauses de Horn sont également présents en PROLOG (le moteur d'inférence étant le mécanisme central de fonctionnement de PROLOG, et la base de clauses le "programme" rédigé par l'utilisateur). Mais en PROLOG les règles de résolution sont implicites (et incluses dans le moteur d'inférences) et se réduisent globalement au classique modus ponens en chainage arrière. L'idée centrale de MOLOG est d'externaliser les règles de résolutions, permettant ainsi de définir le fonctionnement du langage sur des clauses de Horn étendues comprenant des opérateurs modaux.

Les premières versions de MOLOG étaient également des méta-interpréteurs écrits en PROLOG[8], mais la lenteur de PROLOG d'une part et la complexité beaucoup plus importante de la résolution en logique non-classique d'autre part ne permettaient pas de faire fonctionner les programmes MOLOG dans des temps raisonnables.

En 1992, une version[9] de MOLOG fut développée en ADA faisant ainsi le pendant à C-PROLOG, une version de PROLOG écrite en C. Cette version était extrêmement rapide, capable de fonctionner en parallèle sur des réseaux d'ordinateurs, et permettait ainsi de faire de la résolution automatique en logique non-classique dans des temps raisonnables. Le système fut présenté à la grand-messe des systèmes dits de "cinquième génération"[10].

Un classique exemple d'utilisation de MOLOG est la formalisation en logique modale multi-S4 du problème connu en anglais sous le nom de Wise Men Problem, dont voici l'énoncé:

Un roi souhaitait choisir parmi ses trois fils, Gauvin, Lancelot et Arthur, lequel lui succèderait. Pour ce faire, il organisa une épreuve consistant à les réunir tous les trois dans la même pièce, puis à les coiffer chacun d'un heaume soit noir, soit blanc. Chacun des princes était capable de voir la couleur des heaumes des deux autres mais pas la couleur du sien. Le roi s'adressa alors à ses fils et leur dit: "Je puis vous dire qu'il y a dans cette pièce au moins l'un d'entre vous qui porte un heaume blanc." Puis il s'adressa successivement à Gauvin, Lancelot puis Arthur, en leur demandant de quelle couleur était leur heaume. Le premier fut incapable de répondre ainsi que le second. Quant à Arthur, il sut évidemment que son heaume était blanc, et fut ainsi désigné héritier du royaume.

Après avoir brièvement noté que notre roi est un fieffé chenapan qui avait tout arrangé pour qu'Arthur soit son successeur (Lancelot et Gauvin portent des heaumes noirs, et Arthur un heaume blanc, configuration qui garantit le résultat), voyons comment modéliser ce problème en MOLOG.

Nous allons tout d'abord exprimer que tout le monde sait que si le heaume de Gauvin est noir et que le heaume d'Arthur est noir alors le heaume de Lancelot est blanc (hypothèse qu'il y a au moins un heaume blanc):

• NEC(_):((noir(gauvin) et noir(arthur)) → blanc(lancelot))

NEC(X) signifiant X sait que, et NEC(_) signifie tout le monde sait que. NEC est un des opérateurs modaux étendant la logique classique dans le cadre des clauses de Horn étendues. Bien entendu, les deux clauses symétriques doivent être ajoutées au programme:

• NEC(_):((noir(gauvin) et noir(lancelot)) → blanc(arthur))
• NEC(_):((noir(lancelot) et noir(arthur)) → blanc(gauvin))

Il faut ensuite exprimer que tout le monde sait que, si, pour Lancelot, le heaume d'Arthur peut être blanc, alors il est blanc de façon certaine, puisque Lancelot voit le heaume d'Arthur:

• NEC(_):(POS(lancelot):blanc(arthur) → NEC(lancelot):blanc(arthur))

POS(X) est un autre opérateur modal signifiant il est possible pour X que. Cette clause signifie donc, en la lisant de gauche à droite, que tout le monde sait (NEC(_)) que s'il est possible pour lancelot (POS(lancelot)) que le heaume d'Arthur soir blanc (blanc(arthur)) alors (→) Lancelot sait (NEC(lancelot)) que le heaume d'Arthur est blanc (blanc(arthur)). Cette clause doit être complétée par les clauses symétriques de celle-ci, les symétries concernant les trois princes et les deux couleurs. Il faut cependant faire bien attention de ne rien écrire de la forme:

• NEC(_):(POS(lancelot):blanc(lancelot) → NEC(lancelot):blanc(lancelot))

En effet, s'il est possible pour Lancelot que son heaume soit blanc, cela ne lui permet en rien de conclure, car il est incapable de voir son propre heaume, et donc la possibilité du fait n'entraine pas sa certitude.

Il ne reste plus qu'à rajouter les clauses correspondant aux réponses successives des trois princes, clauses qui créent l'asymétrie d'information et permettent ainsi à Arthur de trouver la solution alors que les deux premiers princes ne le peuvent pas:

• NEC(lancelot):POS(gauvin):noir(gauvin)
• NEC(arthur):NEC(lancelot):POS(gauvin):noir(gauvin)
• NEC(arthur):POS(lancelot):noir(lancelot)

La première clause signifie que Lancelot sait qu'il est possible pour Gauvin que Gauvin ait un heaume noir, puisque Gauvin n'a pas pu répondre. La seconde dit qu'Arthur sait que Lancelot sait qu'il est possible pour Gauvin que Gauvin ait un heaume noir. Et la troisième exprime que Arthur sait qu'il est possible pour Lancelot que Lancelot ait un heaume noir.

Le problème ainsi posé est résolu en quelques secondes par MOLOG. Une version du langage avec cet exemple déjà codé est disponible en ligne.

Le langage était rapide et puissant, mais il souffrait de deux défauts majeurs:

• D'une part, le codage de la base de règle de résolutions était complexe. Il devait se faire en ADA, et nécessitait une remarquable connaissance de la résolution automatique en logique modale pour correctement exprimer les règles (ainsi dans l'exemple ci-dessus le problème de la skolémisation des opérateurs modaux a été omis).
• D'autre part, l'expression de la base de clauses n'est pas chose facile dans les logiques non classiques. On voit bien dans l'exemple pourtant simplifié ci-dessus que rédiger un tel programme demande de la finesse et du soin.

• Source de la dernière version de MOLOG, nécessite un compilateur ADA.