--- title: "Searching for Well-Behaved Fragments of Halpern-Shoham Logic" authors: - "Przemysław Andrzej Wałęga" doi: "10.24963/ijcai.2017/769" url: "https://ijcai.org/proceedings/2017/769" pdf: "https://ijcai.org/proceedings/2017/0769.pdf" venue: "Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence" year: 2017 pages: "5219-5220" track: "Doctoral Consortium" keywords: - "Artificial Intelligence: computer science" - "Artificial Intelligence: knowledge representation" - "Artificial Intelligence: artificial intelligence" --- # Searching for Well-Behaved Fragments of Halpern-Shoham Logic Przemysław Andrzej Wałęga *Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence*, pages 5219-5220. DOI: [10.24963/ijcai.2017/769](https://doi.org/10.24963/ijcai.2017/769) ## Abstract Temporal reasoning constitutes one of the main topics within the field of Artificial Intelligence. Particularly interesting are interval-based methods, in which time intervals are treated as basic ontological objects, in opposite to point-based methods, where time-points are considered as basic. The former approach is more expressive and seems to be more appropriate for such applications as natural language analysis or real time processes verification. My research concerns the classical interval-based logic, namely Halpern-Shoham logic (HS). In particular, my investigation continues recently proposed search for well-behaved - i.e., expressive enough for practical applications and of low computational complexity - HS fragments obtained by imposing syntactical restrictions on the usage of propositional connectives in their languages. ## Full text ## 1 Halpern-ShohamLogic and its Fragments Halpern-Shoham logic ([Halpern and Shoham, 1991]) is an elegant multimodal logic for reasoning about time intervals. Time line is modelled as a linear ordering of time-points, and an interval as an ordered pair of points: its beginning and ending points. Modal operators occurring in the language of HS enable us to access an interval that begins (B), is during (D), ends (E), overlaps (O), is adjacent to (A), or is later than (L) the current interval [x, y]. The listed relations are defined as: ![Image](https://ijcai.org/proceedings/2017/fulltext/769/image_000000_343835e9266118c3bf775acb54a30fd55ebfec436d0e240f8df903496cfdba55.png) The further 6 relations are inverses of the above ones. In total, there are 12 relations which give rise to semantics of 12 diamond and 12 box modal operators of the form 〈R〉, and [R], respectively, where R is any of the 12 relations described above. An expression 〈R〉ϕ states that a formula ϕ holds in some interval that is in a relation R with the current interval, and [R]ϕ states that ϕ holds in all intervals that are in a relation R with the current interval. The language of HS is very expressive but the satisfiability problem of its formulas is undecidable [Halpern and Shoham, 1991]. This negative result motivated a search for decidable HS fragments which would be still expressive enough for interesting applications. The recently proposed method for obtaining HS fragments is to syntactically restrict the form of its formulas [Bresolin et al., 2014]. The set of formulas called the Horn fragment of HS (HShorn in short) is defined by the following grammar: where [U] is the universal modality stating that a formula holds in all intervals, and λ is a positive temporal literal: where p is a propositional variable and R is any of 12 relations that can hold between intervals. Further restrictions give rise to the fragment HS ✸horn , which is obtained by deleting an expression of the form [R]λ from the grammar (2), and HS ✷horn is obtained by deleting 〈R〉λ from (2) - see Figure 1 (for the meaning of i and i, @ see the subsequent section). Figure 1: A Hasse diagram in which an edge between HS fragments means that a set of formulas of the fragment that is below is a subset of a set of formulas of the fragment above. ![Image](https://ijcai.org/proceedings/2017/fulltext/769/image_000001_7c32267c19c8ea12a5e7fc29f741632fb312c6467c69703167b4a4ac9653437e.png) The main problem investigated within the research on HS fragments is determining their expressiveness, decidability, and computational complexity. Interestingly, the results depend on the assumed structure of time [Bresolin et al., Forthcoming]. Among the 3 main lines of division, the first one is between: - (Den) Dense time lines - for any time-points x, y such that x < y there is some time-point z such that x < z < y; - (Dis) Discrete time lines - any non-maximal timepoint has an immediate <-successor, and every non-minimal time-point has an immediate <-predecessor. The second distinguishes between: - (S) Strict semantics - punctual intervals, i.e., intervals in which the beginning and ending points coincide, are disallowed; - (Non-S) Non-Strict semantics - punctual intervals are allowed. ## The last line demarcates: - (<) Irreflexive semantics - the ordering "<" exploited in the beginning of the section to define relations between intervals represents an irreflexive greaterthan ordering; - (≤) Reflexive semantics - each occurrence of "<" is replaced by "≤" in the definition of relations under irreflexive semantics, where ≤ represents a greater-or-equal ordering. The most striking result obtained so far is that the satisfiability problem of HS ✷horn -formulas is P-complete under (Den,<,S), (Den,<,Non-S), (Dis,≤,Non-S), (Den,≤,S), and (Den,≤,Non-S) semantics [Bresolin et al., Forthcoming]. Moreover, this fragment was already applied to solve a real-life problem [Kontchakov et al., 2016]. ## 2 My Results and FutureWork As showed in [Areces et al., 2000], full HS is expressive enough to enable referring to a single interval. More precisely, in the language of HS we can define the hybrid machinery [Blackburn, 2000], i.e., nominals - the special sort of atoms each of which is true in exactly one interval, and satisfaction operators @i indexed by nominals and stating that a formula is true in an interval in which a nominal i holds. Intuitively, a nominal labels a single interval and an @i operator enables us to access the interval labelled by i. Referentiality seems to be an important property for a number of applications but it is not clear whether it is expressible in Horn fragments of HS. In [Wał˛ega, 2017] I have proposed adding hybrid machinery, i.e., nominals (denoted by i added to the superscript of fragment's symbol) as well as nominals and @ operators (denoted by i, @ added to the superscript) to HS fragments and to analyse the obtained extensions. The lattice including all these fragments is depicted in Figure 1. My main result concerns computational complexity of HS ✷,i,@ horn and is as follows. Theorem ([Wał˛ega, 2017]) The satisfiability problems of HS ✷,i,@ horn and HS ✷,i horn are NP-complete under (Den,<,S), (Den,<,Non-S), (Dis,≤,Non-S), (Den,≤,S), and (Den,≤,Non-S) semantics. The theorem shows that adding hybrid machinery to HS ✷horn has a price of moving from P-completeness to NPcompleteness, and thus sheds more light on the interplay between expressiveness and computational complexity of HS fragments. As future work I plan to: - Investigate computational complexity of other HS fragments. For instance, one of the unsolved problems is determining computational complexity of HS ✷horn under (Dis,≤,S). At the moment it is not even known if it is decidable; - Study expressiveness of HS fragments. The fragments are intensively scrutinized in terms of their computational complexity but there is hardly any research on their expressiveness; - Search for application domains appropriate for HS fragments and their hybrid versions. ## Acknowledgments This work is supported by the NCN grant DEC2011/02/A/HS1/00395. ## References 1. [Areces et al., 2000] Carlos Areces, Patrick Blackburn, and Maarten Marx. The computational complexity of hybrid temporal logics. Logic Journal of IGPL, 8(5):653-679, 2000. 2. [Blackburn, 2000] Patrick Blackburn. Representation, rea- soning, and relational structures: a hybrid logic manifesto. Logic Journal of the IGPL, 8(3), 2000. 3. [Bresolin et al., 2014] Davide Bresolin, Emilio Muñoz- Velasco, and Guido Sciavicco. Sub-propositional frag- ments of the interval temporal logic of Allen's relations. In European Workshop on Logics in Artificial Intelligence, pages 122-136. Springer, 2014. 4. Bresolin et al., Forthcoming] Davide Bresolin, Agi Kurucz, Emilio Muñoz-Velasco, Vladislav Ryzhikov, Guido Sciav- icco, and Michael Zakharyaschev. Horn fragments of the Halpern-Shoham interval temporal logic. Forthcoming. [Halpern and Shoham, 1991] Joseph Yehuda Halpern and Yoav Shoham. A propositional modal logic of time inter- vals. Journal of the ACM (JACM), 38(4):935-962, 1991. 5. [Kontchakov et al., 2016] Roman Kontchakov, Laura Pan- dolfo, Luca Pulina, Vladislav Ryzhikov, and Michael Za- kharyaschev. Temporal and spatial OBDA with many- dimensional Halpern-Shoham logic. In Proceedings of 25th International Joint Conference on Artificial Intelli- gence (IJCAI-2016). AAAI Press, 2016. 6. [Wałęga, 2017] Przemysław Andrzej Wałęga. Computa- tional complexity of a hybridized Horn fragment of Halpern-Shoham logic. In Indian Conference on Logic and Its Applications, pages 224-238. Springer, 2017.