Dealing with multiple granularity of time in temporal logic programming

Chronolog(MC) is an extension of logic programming based on a linear-time temporal logic with multiple granularity of time called TLC. A Chronolog(MC) program consists of a clock definition, a clock assignment and a program body. Each predicate symbol appearing in the program body is associated with a local clock through the clock definition and assignment. This paper investigates the logical basis of the language, presents a clocked temporal resolution where time-matching is essential, and in particular proposes three algorithms for time-matching. The paper also discusses the declarative semantics of Chronolog(MC) programs in terms of clocked temporal Herbrand models. It is shown that Chronolog(MC) programs also satisfy the minimum model semantics. The language can be used to model a wide range of simulation systems and other relevant tasks where the notion of dynamic change is central.