Predicate logic is a powerful and general descriptive formalism with a long history of development. However, since the logic's underlying semantics have no notion of time, statements such as “I increases by 2” cannot be directly expressed. We discuss interval temporal logic (ITL), a formalism that augments standard predicate logic with operators for time-dependent concepts. Our earlier work used ITL to specify and reason about hardware. In this paper we show how ITL can also directly capture various control structures found in conventional programming languages. Constructs are given for treating assignment, iteration, sequential and parallel computations and scoping. The techniques used permit specification and reasoning about such algorithms as concurrent Quicksort. We compare ITL with the logic-based programming languages Lucid and Prolog.
CITATION STYLE
Moszkowski, B., & Manna, Z. (1984). Reasoning in interval temporal logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 164 LNCS, pp. 371–382). Springer Verlag. https://doi.org/10.1007/3-540-12896-4_374
Mendeley helps you to discover research relevant for your work.