Proposition d’une procédure abductive pour le raisonnement temporel

Eléments d’une procédure abductive pour le raisonnement temporel

Dans le chapitre 3, nous avons vu que toutes les méthodes de génération d’hypothèses étaient basées sur une forme de résolution, linéaire ou SLD. Comme l’on a vu dans le chapitre 2 que l’on pouvait gagner en efficacité, d’abord sur les pas de résolution individuels, puis de manière générale dans le processus d’inférence, en utilisant la résolution avec contraintes, il est légitime d’imposer qu’une procédure abductive basée sur la résolution utilise ce principe de résolution avec contraintes, au besoin en l’adaptant à la forme de résolution qui est utilisée dans la procédure, par exemple la résolution SLD pour les procédures de programmation logique abductive. Parmi toutes les procédures d’abduction que nous avons détaillées précédemment, lesquelles sont les plus adaptées à l’usage que l’on souhaite faire de l’abduction en raisonnement temporel? – Les procédures de Pople (1973) et de (Cox & Pietrzykowsky, 1986) sont utilisables en pratique dans la plupart des cas. Leurs inconvénient est de générer parfois des hypothèses qui sont des formules non closes arbitraires, ce qui peut devenir contradictoire avec l’usage de l’abduction pour la planification, où l’on souhaite plutôt des hypothèses « particulières » pour chaque occurrence d’action ou d’événement ; – Les procédures de programmation logique abductive ont pour inconvénient de ne traiter qu’un sous ensemble de la logique du premier ordre, mais en contrepartie d’être plus simple à implanter et à mettre en œuvre ; – De la mèn e manière, utiliser le cadre de la programmation logique abductive et de la résolution avec contraintes permet o priori d’utiliser bon nombre de résultats (théoriques et pratiques) de la programmation logique avec contraintes, en particulier sur CLP(7?.) (Jaffar, Michaylov, Stuckey, & Yap, 1992b), qui se rapproche le plus de notre usage de la résolution avec des contraintes temporelles ; – La procédure de (Kakas & Mancarella, 1990c) permet d’ajouter à la description du problème des contraintes d’intégrité, ce qui permet d’exclure des combinaisons d’hypothèses, ou d’hypothèses et d’autres conditions, et, par voie de conséquence, de réduire l’espace de recherche. En planification, cela correspond à restreindre dynamiquement les possibilités d’occurrence de certaines actions ; – A contrario la procédure SLDNFA ne manipule pas de contraintes d’intégrité : ce qui se comprend car elle a été principalement utilisée avec le calcul d’événements, qui ne contient pas de telles clauses : l’usage de la négation par échec est ici suffisant. Si l’on souhaite être relativement indépendant du langage (formalisme) temporel utilisé, cela peut être u n facteur limitant l’intérêt de SLDNFA.  

Description de la procédure

Avant de décrire notre procédure, il semble nécessaire de revenir sur la procédure abductive de Kakas et Mancarella (K&M) décrite dans (Kakas & Mancarella, 1990c), et seulement entrevue dans le chapitre 3. En effet, le principe général de cette procédure est identique à celle qui sera décrite ici, et la procédure de K&M est aussi plus simple que la nôtre, ce qui facilite donc la présentation. Après avoir décrit et analysé cette procédure, nous étudierons comment celle-ci peut être adaptée au raisonnement temporel, en incorporant l’usage d’un principe de résolution avec contraintes. 4.2.1 La procédure originale de K&M : défauts et remèdes Pour (Kakas & Mancarella, 1990c), un problème d’abduction est décrit par un triplet (P, IC, A) où P est un programme logique, IC est un ensemble de clauses sans tête appelées contraintes d’intégrité, et A est un ensemble de symboles de prédicats utilisés dans P et que l’on appelle supposables. Si <~ Q est un but, l’objet de la procédure est de trouver un ensemble d’hypothèses A (instances closes de prédicats supposables, notés avec le signe ‘) tel que – P U A j= Q, c’est à dire que Q est vrai dans tout modèle de P U A ; – P U A ¡= IC, c’est à dire que toutes les clauses de IC sont vraies dans tous les modèles de P U A. La notion de modèle pour un programme logique retenue par K&M est celle de modèle stable (Gelfond & Lifschitz, 1988). Satisfaire les contraintes d’intégrité est donc fortement lié à la sémantique associée aux programmes logiques. Comme cela a été décrit dans le chapitre 3, K&M transforment préalablement le triplet (P,A,IC) en un nouveau triplet (P*,A*,IC*) obtenu par réécriture des littéraux négatifs dans le corps des clauses. Tout littéral négatif ~a est remplacé par un littéral a*, qui représente donc l’opposé de a, et a* est ajouté à l’ensemble des littéraux supposables A. Cette transformation n’est pas strictement indispensable pour présenter la procédure, et nous ne l’appliquerons pas dans ce qui suit. Sont donc considérés comme supposables tous les littéraux négatifs et les littéraux positifs référencés comme tels par l’ensemble A. On suppose implicitement que 92 Chapitre 4. Proposition d’une procédure abductive l’ensemble des contraintes d’intégrité IG contient pour chaque littéral supposable a une contrainte de la forme *r-a,^a. Quel que soit le signe d’un littéral, on garde la notation ~ a pour désigner son opposé. On suppose aussi que l’on se donne une règle de sélection des littéraux dans le corps d’une clause : cette règle est notée 1Z. Définition formelle de la procédur e de K& M La procédure entrelace deux types de dérivation : le premier type s’appelle dérivation abductive et a pour objet de réécrire une clause but à l’aide des règles du programme, et d’identifier les littéraux susceptibles d’être supposés. Lorsqu’un de ces littéraux est rencontré, il n’est acceptable comme hypothèse que lorsqu’il est consistant. Conformément à la définition choisie, la consistance d’une hypothèse signifie que toutes les contraintes d’intégrité sont satisfaites dans un modèle du programme augmenté des hypothèses. Définition 4-1 (dérivation abductive ) (Kakas & Mancarella, 1990c) Une dérivation abductive de (Gi,Ai) à (Gn,An) est une séquence de paires (G¿,A¿) telle que pour tout i, Gi est de la forme <— L±,…, Lk, le littéral Lj est sélectionné par 1Z dans Gi, A¿ est un ensemble de littéraux supposables et sans variables, et Pune des trois conditions suivantes est vérifiée : (A\) Lj est non supposable, C est un résolvant de Gi et d! une clause de P sur le littéral Lj, alors : Gi+i = C Ai+i = Ai (Â2) Lj est supposable, Lj S A¿, alors: Gi+i =*— L\,…, Lj„i,Lj+i,…, Lk A,+i = A, (Az) Lj est supposable, Lj g A, et ~Lj <£ A,, il existe une dérivation de consistance de ({Lj}, Ai U{Lj}} à ({},A’), alors: Gi+i =*— L\,.., ,Lj-i,Lj+i,… ,Lk Aj + i = A Par rapport à la résolution SLDNF classique (ou encore PROLOG avec une règle de sélection des littéraux), le cas Ai n’est qu’un pas de résolution classique pour réécrire le but courant Gi à l’aide d’une règle qui conclut sur le prédicat Lj ; le cas A2 correspond au cas où Lj est déjà présent dans l’ensemble des hypothèses, il est alors supposé vrai et effacé dans le bu t G¿ ; et Az est appelé lorsqu’on désire faire l’hypothèse Lj. Il faut en particulier que ni Lj ni son opposé ne soient présents dans 4.2. Description de la procédure 93 Ai : Lj sera accepté comme hypothèse si le test de consistance réussit, autrement dit si il existe une dérivation de consistance à partir de ce littéral. Définition 4.2 (dérivation de consistance ) (Kakas & Mancarelîa, 1990c) Une dérivation de consistance pour un littéral supposable a est une séquence de paires ({a},Ao), {-Fi,AÏ), … , (Fn,An) telle que: (i) Fi est l’union de tous les buts obtenus en résolvant la clause a <— avec les contraintes d’intégrité, et A i = Ao; (ii) pour ¿ > 1, l’ensemble Fi est de la forme {<— L\,…, L^} U F¡ et il existe j € [l,k] tel que l’on obtient (Fî + i, A¿+i) par une des quatre conditions suivantes: (Ci) Lj est non supposable, C est l’ensemble de tous les résolvants du but <— L\,…, Lk avec les clauses de P sur le littéral Lj, la clause vide D n’appartient pas à C, et on a: Ft+1 = C U fi A i + 1 = Ai (C%) Lj est supposable, Lj 6 A „ k > 1, alors : Fi+i = {^ Li,…, Lj^i, Lj+i,…, Lk] U F¡ Aj + i = A¿ (C¡) Lj est supposable, l’opposé de Lj appartient à A¿, alors : Fi+l = F¡ A I + i = A¿ (C\) Lj est supposable, ni Lj ni son opposé n’appartiennent à Ai, et il existe une réfutation abductive de {+-~Lj,Ai) à (D,A’}, alors: Fi+i = F¡ Ai+i = A’ Le but d’une dérivation de consistance est de vérifier qu’un littéral clos a peut être ajouté aux hypothèses déjà faites. Pour ceci, il faut que les contraintes d’intégrité soient vérifiées: c’est l’objet du passage de FQ à i*\. Pour le littéral a dont on souhaite faire une hypothèse, c’est à dire le considérer vrai, une contrainte d’intégrité <— a, Li,…, Ln sera satisfaite dès lors qu’un des littéraux Li ne sera pas vrai, ce qui signifie qu’il sera non prouvable : on cherche donc l’échec du but *— L\,…, Ln. Cette technique est reprise de celle développée par (Sadri & Kowalski, 1988), pour vérifier la satisfaction de contraintes d’intégrité lors d’opérations sur une base de données deductive. Une fois acquis le principe que Fi représente un ensemble de buts que l’on veut voir échouer, tous les cas de la dérivation sont des moyens d’y arriver. Un échec sur une clause signifie que cette clause est enlevée de l’ensemble F¿,