Représentation logique et traitement algorithmique du temps

Notre intelligence finie ne nous permet pas de mettre en oeuvre les explications précises que la nature fournit sur les relations temporelles des évènements qui produisent d'une manière continuelle des impressions que nos sens éprouvent. Tant il est vrai que, le plus souvent, l'évaluation approximative des impressions qui se produisent en nous à l'occurrence d'un évènement importe bien davantage que leur appréciation exacte. Il s'ensuit que le problème de la représentation logique et du traitement algorithmique du temps est celui des exigences commandées par l'accumulation des problèmes pratiques liés aux questions qui prêtent à discussion chaque fois que l'étude qualitative des relations des évènements qui remplissent le temps prime plutôt que leur étude quantitative. C'est pourquoi la découverte de modèles qualitatifs de raisonnement sur le temps est une tâche à laquelle beaucoup s'intéressent. Il est clair que le modèle des intervalles développé par Allen est le plus connu de tous les modèles qualitatifs de raisonnement sur le temps.

Au sujet des modèles mathématiques du temps élaborés par Allen, le coeur du problème consiste dans les qualités spécifiques qui distinguent entre elles certaines des relations des intervalles qui les composent, à l'exemple de la relation "rencontre" qui est vraie entre deux intervalles lorsque la fin de l'un est confondue avec le début de l'autre. Elles sont multiples, les applications à l'informatique et à l'intelligence artificielle des modèles qualitatifs de raisonnement sur le temps que nous venons d'évoquer. Toujours est-il, le modèle des intervalles ne permet pas de rendre compte des relations temporelles entre évènements interruptibles. C'est pourquoi la découverte de nouveaux modèles qualitatifs de raisonnement sur le temps est une tâche à laquelle il faut s'intéresser fortement. Mais il faut voir au préalable ce que nous entendons par "représentation logique et traitement algorithmique du temps".

Par "représentation logique du temps", nous concevons toute logique formelle dont les modèles sont des modèles mathématiques du temps et dans lesquels nous ne pouvons connaître que les relations des éléments qui les composent. Il en résulte que la logique classique et la logique modale conviennent mieux que toute autre logique formelle à l'élaboration d'un langage de représentation logique du temps permettant de formuler les propriétés de ces relations. Nous examinerons certaines des logiques classiques et des logiques modales qui sont les solutions que les mathématiques et la logique ont apportées au problème de l'analyse rationnelle de notre perception du temps, et nommément, les logiques classiques et les logiques modales dont les modèles sont des ordres linéaires. Pour faire la différence entre tous ces modèles, nous considèrerons les propriétés que vérifient les relations des éléments qui les composent : la relation "est plus petit que" entre les points d'un ordre linéaire et la relation "rencontre" entre les intervalles d'un ordre linéaire.

En écrivant "traitement algorithmique du temps", nous pensons à toute méthode de décision capable d'imaginer en un temps raisonnable la démonstration d'un certain nombre de théorèmes parmi les théorèmes des logiques classiques et des logiques modales dont nous venons de parler. Bien sûr, il y a dans les modèles mathématiques du temps des formes particulières sous lesquelles se présentent les relations des éléments qui les composent, qui favorisent tel type de méthodes plutôt que tel autre.

Expressivité des logiques formelles qui solutionnent le problème de l'analyse rationnelle de notre perception du temps, efficacité des méthodes de décision qui solutionnent le problème de la mécanisation du raisonnement sur le temps : les principes qui président à la préparation de cet exposé nous conduisent à l'adoption d'un plan en 3 parties. Parce que notre perception du temps nous amène immanquablement à étudier la relativité des moments des évènements qui remplissent le temps, nous parlerons d'abord de logique classique du premier ordre. Afin d'exprimer certaines propriétés de la relation "est plus petit que" entre les points d'un ordre linéaire, nous parlerons ensuite de logique classique du second ordre. Pour constituer un fragment traitable de la logique classique du second ordre, nous parlerons ensuite de logique modale propositionnelle.

Références

[1] J. Allen. Maintening knowledge about temporal intervals. Communications of the ACM, Volume 26, 832-843, 1983.

[2] E. Audureau, L. Farinas del Cerro, P. Enjalbert. Logique temporelle : sémantique et validation de programmes parallèles. Masson, 1990.

[3] J. van Benthem. The Logic of Time. Kluwer, 1983.

[4] H. Bestougeff, G. Ligozat. Outils logiques pour le traitement du temps : de la linguistique à l'intelligence artificielle. Masson, 1989.

[5] R. Fagin, J. Halpern, Y. Moses, M. Vardi. Reasoning About Knowledge. MIT Press, 1995.

[6] J.-L. Gardies. La logique du temps. Presses universitaires de France, 1975.

[7] H. Kamp. Tense Logic and the Theory of Linear Order. Thèse de l'université de Californie à Los Angeles, 1968