Sub-propositional fragments of the interval temporal logic of Allen’s relations. (English) Zbl 1432.03028
Fermé, Eduardo (ed.) et al., Logics in artificial intelligence. 14th European conference, JELIA 2014, Funchal, Madeira, Portugal, September 24–26, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8761, 122-136 (2014).
Summary: Interval temporal logics provide a natural framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as the primitive ontological entities. The most influential propositional interval-based logic is probably Halpern and Shoham’s modal logic of time intervals, a.k.a. HS. While most studies focused on the computational properties of the syntactic fragments that arise by considering only a subset of the set of modalities, the fragments that are obtained by weakening the propositional side have received very scarce attention. Here, we approach this problem by considering various sub-propositional fragments of HS, such as the so-called Horn, Krom, and core fragment. We prove that the Horn fragment of HS is undecidable on every interesting class of linearly ordered sets, and we briefly discuss the difficulties that arise when considering the other fragments.
For the entire collection see [Zbl 1296.68009].
For the entire collection see [Zbl 1296.68009].
References:
| [1] | Allen, J. F., Maintaining knowledge about temporal intervals, Communications of the ACM, 26, 11, 832-843 (1983) · Zbl 0519.68079 · doi:10.1145/182.358434 |
| [2] | Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: DL-lite in the light of first-order logic. In: Proc. of the 22nd AAAI Conference on Artificial Intelligence, pp. 361-366 (2007) |
| [3] | Artale, A.; Kontchakov, R.; Ryzhikov, V.; Zakharyaschev, M.; McMillan, K.; Middeldorp, A.; Voronkov, A., The complexity of clausal fragments of LTL, Logic for Programming, Artificial Intelligence, and Reasoning, 35-52 (2013), Heidelberg: Springer, Heidelberg · Zbl 1433.03046 · doi:10.1007/978-3-642-45221-5_3 |
| [4] | Artale, A., Ryzhikov, V., Kontchakov, R., Zakharyaschev, M.: A cookbook for temporal conceptual data modelling with description logics. ACM Transaction on Computational Logic (TOCL) (To appear) · Zbl 1354.68245 |
| [5] | Bresolin, D.; Della Monica, D.; Goranko, V.; Montanari, A.; Sciavicco, G.; Cervesato, I.; Veith, H.; Voronkov, A., Decidable and undecidable fragments of Halpern and Shoham’s interval temporal logic: towards a complete classification, Logic for Programming, Artificial Intelligence, and Reasoning, 590-604 (2008), Heidelberg: Springer, Heidelberg · Zbl 1182.03037 · doi:10.1007/978-3-540-89439-1_41 |
| [6] | Bresolin, D., Della Monica, D., Goranko, V., Montanari, A., Sciavicco, G.: The dark side of interval temporal logic: sharpening the undecidability border. In: Proc. of the 18th International Symposium on Temporal Representation and Reasoning (TIME), pp. 131-138. IEEE Comp. Society Press (2011) · Zbl 1325.03014 |
| [7] | Bresolin, D., Della Monica, D., Montanari, A., Sala, P., Sciavicco, G.: Interval temporal logics over strongly discrete linear orders: the complete picture. In: Proc. of the 4th International Symposium on Games, Automata, Logics, and Formal Verification (GANDALF). EPTCS, vol. 96, pp. 155-169 (2012) · Zbl 1469.03045 |
| [8] | Bresolin, D.; Goranko, V.; Montanari, A.; Sala, P., Tableau-based decision procedures for the logics of subinterval structures over dense orderings, Journal of Logic and Computation, 20, 1, 133-166 (2010) · Zbl 1188.03009 · doi:10.1093/logcom/exn063 |
| [9] | Bresolin, D.; Monica, D. D.; Montanari, A.; Sciavicco, G., The light side of interval temporal logic: the Bernays-Schönfinkel fragment of CDT, Annals of Mathematics and Artificial Intelligence, 71, 1-3, 11-39 (2014) · Zbl 1325.03015 · doi:10.1007/s10472-013-9337-y |
| [10] | Bresolin, D., Montanari, A., Sala, P., Sciavicco, G.: What’s decidable about Halpern and Shoham’s interval logic? the maximal fragment \(\mathsf{AB\overline{B}\overline{L}} \). In: Proc. of the 26th IEEE Symposium on Logic in Computer Science (LICS), pp. 387-396. IEEE Computer Society (2011) |
| [11] | Chaochen, Z., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. EATCS: Monographs in Theoretical Computer Science. Springer (2004) · Zbl 1071.68062 |
| [12] | Chen, C.; Lin, I., The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic, Information Processing Letters, 3, 45, 131-136 (1993) · Zbl 0796.68116 · doi:10.1016/0020-0190(93)90014-Z |
| [13] | Chen, C.; Lin, I., The computational complexity of the satisfiability of modal Horn clauses for modal propositional logics, Theoretical Computer Science, 129, 1, 95-121 (1994) · Zbl 0808.03025 · doi:10.1016/0304-3975(94)90082-5 |
| [14] | Fariñas Del Cerro, L.; Penttonen, M., A note on the complexity of the satisfiability of modal Horn clauses, Journal of Logic Programming, 4, 1, 1-10 (1987) · Zbl 0624.03010 · doi:10.1016/0743-1066(87)90018-5 |
| [15] | Fisher, M.: A resolution method for temporal logic. In: Proc. of the 12th International Joint Conference on Artificial Intelligence (IJCAI), pp. 99-104. Morgan Kaufman (1991) · Zbl 0745.68091 |
| [16] | Halpern, J.; Shoham, Y., A propositional modal logic of time intervals, Journal of the ACM, 38, 4, 935-962 (1991) · Zbl 0799.68175 · doi:10.1145/115234.115351 |
| [17] | Marcinkowski, J., Michaliszyn, J.: The ultimate undecidability result for the Halpern-Shoham logic. In: Proc. of the 26th IEEE Symposium on Logic in Computer Science (LICS), pp. 377-386. IEEE Comp. Society Press (2011) |
| [18] | Montanari, A.; Puppis, G.; Sala, P.; Abramsky, S.; Gavoille, C.; Kirchner, C.; Meyer auf der Heide, F.; Spirakis, P. G., Maximal decidable fragments of Halpern and Shoham’s modal logic of intervals, Automata, Languages and Programming, 345-356 (2010), Heidelberg: Springer, Heidelberg · Zbl 1288.03017 · doi:10.1007/978-3-642-14162-1_29 |
| [19] | Montanari, A., Puppis, G., Sala, P., Sciavicco, G.: Decidability of the interval temporal logic \(\mathsf{AB\overline{B}}\) on natural numbers. In: Proc. of the 27th Symposium on Theoretical Aspects of Computer Science (STACS), pp. 597-608. Inria Nancy Grand Est & Loria (2010) · Zbl 1230.03047 |
| [20] | Moszkowski, B.: Reasoning about digital circuits. Tech. rep. stan-cs-83-970, Dept. of Computer Science, Stanford University, Stanford, CA (1983) |
| [21] | Nalon, C.; Dixon, C., Clausal resolution for normal modal logics, Journal of Algorithms, 62, 3-4, 117-134 (2007) · Zbl 1131.03007 · doi:10.1016/j.jalgor.2007.04.001 |
| [22] | Nguyen, L., On the complexity of fragments of modal logics, Advances in Modal Logic, 5, 318-330 (2004) · Zbl 1361.68031 |
| [23] | Pratt-Hartmann, I., Temporal prepositions and their logic, Artificial Intelligence, 166, 1-2, 1-36 (2005) · Zbl 1132.03334 · doi:10.1016/j.artint.2005.04.003 |
| [24] | Sipser, M.: Introduction to the theory of computation. PWS Publishing Company (1997) · Zbl 1169.68300 |
| [25] | Sistla, A.; Clarke, E., The complexity of propositional linear temporal logic, Journal of the ACM, 32, 733-749 (1985) · Zbl 0632.68034 · doi:10.1145/3828.3837 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
