DEALING WITH MULTIPLE GRANULARITY OF TIME IN TEMPORAL LOGIC PROGRAMMING

Chronolog(MC) is an extension of logic programming based on a linear-t ime temporal logic with multiple granularity of time called TLC. A Chr onolog(MC) program consists of a clock definition, a clock assignment and a program body. Each predicate symbol appearing in the program bod y is associated with a local clock through the clock definition and as signment. This paper investigates the logical basis of the language, p resents a clocked temporal resolution where time-matching is essential , and in particular proposes three algorithms for time-matching. The p aper also discusses the declarative semantics of Chronolog(MC) program s in terms of clocked temporal Herbrand models. It is shown that Chron olog(MC) programs also satisfy the minimum model semantics. The langua ge can be used to model a wide range of simulation systems and other r elevant tasks where the notion of dynamic change is central. (C) 1996 Academic Press Limited.