Implantation de la procédure abductive

Dans ce chapitre, nous étudions brièvement l’implantation de la procédure de preuve. Ce qui suit est dicté par les enseignements tirés de l’implantation d’un proto­ type de la procédure. Nous décrivons tout d’abord le cadre général de l’implantation, en particulier l’introduction du typage, puis nous présentons un algorithme incré­ mental et efficace pour la gestion de contraintes temporelles métriques. Pour finir, nous étudions la faisabilité d’une machine abstraite pour l’exécution de la procédure abductive. H y a plusieurs possibilités pour l’implantation de la procédure abductive. Une première solution est d’en faire un méta-interprète au dessus de Prolog, comme c’est le cas pour le planificateur CHICA de Missiaen. Cette solution présente l’avantage d’utiliser un cadre où la résolution SLD est déjà implantée, et où le parcours de l’espace de recherche est une notion naturelle. Par contre, Prolog souffre de sa trop grande simplicité, en particulier de son absence de système de typage natif et bien intégré. Nous avons pu voir, durant la description de la procédure, que beaucoup de notions devaient être adaptées à la sémantique des termes utilisés : par exemple, l’égalité ne s’interprète pas de la même manière entre deux instants, qu’entre deux événements, ou entre deux robots. Dans le premier cas, cette égalité signifie que les deux instants sont à la même position sur une droite temporelle, alors que dans le calcul d’événements, où chaque événement est représenté par un terme, l’égalité entre deux événements est équivalente à l’égalité (isomorphic) entre les deux termes.

L’introduction des types dans la programmation logique, et en particulier pour le langage Prolog, a reçu beaucoup d’attention et fait l’objet de nombreux travaux. On peut citer le système de (Mycroft & O’Keefe, 1984), dont (Lakshman & Reddy, 1991) présente une reconstruction formelle. L’inconvénient de beaucoup de ces sy- tèmes est l’absence de possibilités de sous-typage, car celle-ci détruit la propriété de « consistance des types ». Cette propriété signifie que l’application d’une règle d’inférence, la résolution SLD dans ce cas, à des expressions (clauses) bien formées produit une expression bien formée, ce qui dispense de la vérification des types lors de l’exécution (Deitrich & Hagl, 1988). H faut noter qu’une des motivations de H.J. Bûrckert pour la mise au point du mécanisme général de la résolution avec contraintes était d’utiliser des systèmes comme KL-ONE (Brachman & Levesque, 1985) pour représenter les connaissances taxonomiques d’un domaine particulier, en parallèle avec des systèmes déductifs basés sur la résolution. Dans cette approche, les descriptions de typage, les relations entre les types des termes, sont des contraintes dont la satisfaisabilité est déterminée à l’aide d’un système à la KL-ONE.

Notre solution est plus proche de cette dernière que des extensions habituelles de la programmation logique par des types. De la même manière que Bûrckert, la résolution SLD avec contraintes est utilisée aussi avec des contraintes de typage sur les termes des clauses. Chaque clause est donc associée à des contraintes temporelles, à des contraintes de typage et éventuellement à des contraintes de domaine. Ces contraintes sont combinées lors du calcul de résolvant et leur consistance est vérifiée en évaluant le type des termes et en le comparant à celui indiqué par la contrainte de typage. H n’y a pas d’interaction entre ce système de contraintes de typage et les contraintes temporelles, et la consistance globale est équivalente à la consistance de chaque type de contraintes, si l’on ne prend pas en compte les contraintes sur domaines finis. Nous définissons les informations taxonomiques à l’aide d’une hiérarchie de types, qui sont représentés par des symboles, et chaque symbole de fonction et de prédicat est associé à une signature. Les variables sont déclarées avec un type lors de l’écriture des clauses. Par exemple, pour le calcul d’événements, les types et les signatures sont définis sur la figure 5.1.