A separation theorem for discrete-time interval temporal logic. Issue 1 (2nd January 2022)

• Record Type: Journal Article
• Authors: Guelev, Dimitar P.; Moszkowski, Ben
• Is Part Of: Journal of applied non-classical logics. Volume 32:Issue 1(2022)
• Page Start: 28
• Page End: 54
• Publication Date: 2022-01-02
• Subjects: Gabbay separation -- interval temporal logic -- expanding modalities; Nonclassical mathematical logic -- Periodicals; Wiskundige logica; Logic; Periodicals; 511.3105
• DOI: 10.1080/11663081.2022.2050135
• Languages: English
• ISSNs: 1166-3081

Abstract

Abstract : Gabbay's separation theorem about linear temporal logic with past has proved to be one of the most useful theoretical results in temporal logic. In this paper, we establish an analogous statement about Moszkowski's discrete-time propositional Interval Temporal Logic ( I T L ) with two sets of expanding modalities, namely the unary neighbourhood modalities and the binary weak inverses of I T L 's chop operator. We prove that separation holds for I T L both with and without its loop construct chop-star .