CONSTRAINED RESOLUTION AND ABDUCTIVE TEMPORAL REASONING

This article presents our work on the effective implementation of abdu ction in temporal reasoning. This works builds on some results, both i n the logic programming field and in the automated reasoning area. We have defined and implemented an abductive procedure, which is well ada pted for temporal reasoning because it is based on a constrained resol ution principle. Constrained resolution has two advantages for tempora l reasoning: First, it allows us to deal efficiently with temporal ord ering and equality predicates, which are otherwise too much trouble wi th classical resolution; second, it allows a restricted form of abduct ion where hypotheses are limited to ordering relationships. From the l ogic programming area, our work uses results and procedures developed by others in the abductive logic programming field. The procedure we d efine and implement in this work is relatively independent of the temp oral formalism: It has been used with some reified temporal logics and with the event calculus. More generally it can be used on any point-b ased temporal formalism, provided that a correct and complete algorith m is available for checking the consistency of a set of temporal order ing relationships in this language.