Reasoning with ´And Then´ and ´While´

Interval-based temporal logics are natural frameworks for modeling a number of problems from various areas of computer science such as artificial intelligence, natural language processing, temporal databases and formal specification. Quite a few interval-based temporal logics became popular in recent years, such as Venema´s CDT logic, Halpern and Shoham´s HS logic, Moszkowski´s ITL and its prepositional version, and Goranko, Montanari, and Sciavicco ´s PNL. In this work we introduce a new prepositional interval-based temporal logic called CW, which can be considered an extension of the prepositional fragment of Moszkowski´s ITL evaluated over different (parallel) lines, and which is particularly adapt for expressing natural language sentences. We study the logic CW and develop a (non-terminating) sound and complete deduction system based on tableaux for it.