Résolution et logiques temporelles

Motivations

A ce point de notre exposé, le paysage est le suivant: l’on dispose d’une variété de langages permettant l’expression du temps et de concepts liés au temps, et ces langages peuvent être classés suivant la figure 2.1 par ordre d’expressivité croissante. En vis à vis de cette classification, inspirée de (Vila, 1994), nous avons porté des indications sur l’existence d’une procédure de test de la satisfiabilité, et dont le coût serait polynomial. Cette classification est bien entendue très schématique, puisqu’il existe malgré tout des procédures de preuve pour des langages comme la logique ETL de (Sandewall, 1988a), par exemple. Encore ce dernier langage est-il assez limité syntaxiquement, et la procédure correspondante a un coût qui peu t devenir exponentiel. Néanmoins, il existe un seuil d’expressivité en delà duquel la mise en pratique du raisonnement temporel devient très difficile. A quels problèmes se heurte cette mise ? PC2 : correct PC2 : correct et complet 2.1. Motivations 45 en œuvre ¡ efficacité : Il est évident qu’une procédure de preuve polynomiale ne peut s’envisager que pour un langage très restreint, comme l’algèbre d’instants. Néanmoins, en abandonnant cette exigence sur le coût d’une procédure, et donc en se tournant vers des techniques utilisées en démonstration automatique ou en programmation logique, on reste confronté à un manque d’efficacité non négligeable. Ce problème sera plus particulièrement examiné dans la suite de ce chapitre; persistanc e : la persistance est un exemple typique de raisonnement par défaut. Cette constatation débouche alors sur tout le cortège de problèmes pratiques rencontrés lors de la mise en pratique de tels modes de raisonnement. Faut-il utiliser des sémantiques préférentielles (Haugh, 1987b; Shoham, 1988; Sandewall, 1988b), sachant que l’implantation en est très difficile (Hansson, 1990), ou s’orienter vers le raisonnement hypothétique comme le pense (Poole, 1988)? sémantiqu e no n classique : les logiques temporelles réifiées, de même que celles que l’on peut construire par la méthode des arguments temporels (Haugh, 1987a), ont une sémantique qui n’est pas habituelle, où l’habitude désigne la sémantique Tarskienne de ia logique du premier ordre. En particulier, et ceci est important si l’on songe à appliquer des méthodes de démonstration inspirées de la programmation logique, les structures d’interprétations proposées pour ces langages ne sont pas des interprétations de Herbrand. C’est à dire que certains termes ne peuvent pas être liés à eux mêmes par le processus d’interprétation. Ceci est particulièrement visible dans le cas des logiques temporelles réifiées que décrit Shoham (1987). 

Des difficultés de la résolution avec des logiques temporelles

Si l’intérêt du principe de résolution comme mécanisme d’inférence n’est plus à établir, en revanche sa mise en œuvre se heurte souvent à des problèmes induits par certaines caractéristiques des théories manipulés : présence ou non d’un prédicat d’égalité, clauses auto-résolvantes, etc. Ces caractéristiques multiplient les possibilités de résolution et contribuent à augmenter significativement la taille de l’espace de recherche. Ces problèmes doivent être résolus au niveau du contrôle de lïnférence par le biais de stratégies et d’heuristiques adaptées. Il y a deux raisons qui limitent l’usage de la résolution« et plus généralement d’un démonstrateur générique par résolution, comme OTTER (McCune, 1990), pour le raisonnement temporel. Le premier problème vient de l’usage de relations d’ordre entre les instants, ainsi que de l’égalité. Le deuxième est plus général et provient de la difficulté qu’il y a à modéliser une persistance « par défaut » avec une sémantique classique non préférentielle.

Relations d’ordre et d’égalité

L’utilisation des symboles de reiation < et < suppose que l’on soit capable de raisonner avec les relations d’ordre et d’égalité dans un mécanisme par résolution. Pour l’égalité, les solutions proposées dans la littérature, celles bâties autour de la paramodulatîon (Wos & Robinson, 1970), ou des systèmes de réécriture (Hsiang, 1987), sont en général lourdes et coûteuses. En ce qui concerne la relation d’ordre <, les axiomes qui la définissent ont, lorsqu’ils sont écrits sous forme clai’sale, le même défaut que les axiomes d’égalité, c’est à dire que ces clauses sont auto-résolvantes {sdf-resolving) : deux copies d’une même clause (par renommage des variables) peuvent produire un résolvant, qui, de manière générale, a peu de chances d’être utile pour mie déduction particulière.

Tout n’est pas toujours vrai…

Le deuxième problème posé par l’usage d’un démonstrateur de théorèmes pour le raisonnement temporel est lié à la difficulté qu’il y a à formaliser la persistance de telle manière que les effets attendus d’un scénario soient des théorèmes de la théorie logique qui formalise le scénario, c’est à dire des formules vraies dans tous les modèles. L’exemple qui suit illustre ceci. Cet exemple est décrit dans un langage qui est une logique temporelle réifiée très simple, dans laquelle nous donnerons une formalisation possible de la persistance. Cette logique ne permet que de qualifier des propositions par des points ou des intervalles, ceux-ci étant désignés à l’aide de leur deux points extrémités. L’exemple à traiter suppose un raisonnement sur la persistance d’une information.