A New Unification Method for Temporal Reasoning with Constraints

Abstract

In this work we consider using logic programs to perform temporal reasoning. We identify some difficulties of combining constraint propagation and generalized resolution when temporal information is represented using tokens. We show that standard top-down evaluation (i.e. resolution) is incomplete due to the inability to unify constraints and ground terms. We present some syntactic restrictions that enable temporal resolution. Under these restrictions, we propose a new unification method composed of constraint unification and token fusion algorithms. Incorporating them within a generalized resolution scheme render it complete.