Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions. (English) Zbl 1221.03022
Summary: We investigate the expressiveness of the variety of propositional interval neighborhood logics (PNL), we establish their decidability on linearly ordered domains and some important subclasses, and we prove the undecidability of a number of extensions of PNL with additional modalities over interval relations. Altogether, we show that PNL form a quite expressive and nearly maximal decidable fragment of Halpern-Shoham’s interval logic HS.
MSC:
| 03B70 | Logic in computer science |
| 03B25 | Decidability of theories and sets of sentences |
| 03B44 | Temporal logic |
Keywords:
neighborhood interval logics; expressiveness; two-variable fragment; decidability; undecidabilityReferences:
| [1] | Börger, E.; Grädel, E.; Gurevich, Y., Perspectives of Mathematical Logic (1997), Springer · Zbl 0865.03004 |
| [2] | D. Bresolin, V. Goranko, A. Montanari, P. Sala, Tableau-based decision procedure for the logic of proper subinterval structures over dense orderings, in: C. Areces, S. Demri (Eds.), Proc. of the 5th International Workshop on Methods for Modalities, M4M, 2007, pp. 335-351; D. Bresolin, V. Goranko, A. Montanari, P. Sala, Tableau-based decision procedure for the logic of proper subinterval structures over dense orderings, in: C. Areces, S. Demri (Eds.), Proc. of the 5th International Workshop on Methods for Modalities, M4M, 2007, pp. 335-351 · Zbl 1133.03007 |
| [3] | Bresolin, D.; Goranko, V.; Montanari, A.; Sala, P., Tableau systems for logics of subinterval structures over dense orderings, (Olivetti, N., Proc. of TABLEAUX 2007. Proc. of TABLEAUX 2007, LNAI, vol. 4548 (2007), Springer), 73-89 · Zbl 1133.03007 |
| [4] | Bresolin, D.; Montanari, A., A tableau-based decision procedure for Right Propositional Neighborhood Logic, (Proc. of TABLEAUX 2005. Proc. of TABLEAUX 2005, LNAI, vol. 3702 (2005), Springer), 63-77 · Zbl 1141.03307 |
| [5] | Bresolin, D.; Montanari, A.; Sala, P., An optimal tableau-based decision algorithm for Propositional Neighborhood Logic, (Proc. of 24th International Symposium on Theoretical Aspects of Computer Science. Proc. of 24th International Symposium on Theoretical Aspects of Computer Science, STACS. Proc. of 24th International Symposium on Theoretical Aspects of Computer Science. Proc. of 24th International Symposium on Theoretical Aspects of Computer Science, STACS, LNCS, vol. 4393 (2007), Springer), 549-560 · Zbl 1141.03308 |
| [6] | Bresolin, D.; Montanari, A.; Sala, P.; Sciavicco, G., Optimal tableaux for right propositional neighborhood logic over linear orders, (Proc. of the 11th European Conference on Logics in AI. Proc. of the 11th European Conference on Logics in AI, JELIA. Proc. of the 11th European Conference on Logics in AI. Proc. of the 11th European Conference on Logics in AI, JELIA, LNAI, vol. 5293 (2008), Springer), 62-75 · Zbl 1178.03030 |
| [7] | Bresolin, D.; Montanari, A.; Sciavicco, G., An optimal decision procedure for Right Propositional Neighborhood Logic, Journal of Automated Reasoning, 38, 1-3, 173-199 (2007) · Zbl 1121.03027 |
| [8] | Etessami, K.; Vardi, M. Y.; Wilke, T., First-order logic with two variables and unary temporal logic, Information and Computation, 179, 2, 279-295 (2002) · Zbl 1096.03013 |
| [9] | Gabbay, D. M.; Hodkinson, I. M.; Reynolds, M., Temporal Logic: Mathematical Foundations and Computational Aspects (1994), Oxford University Press · Zbl 0921.03023 |
| [10] | Goranko, V.; Montanari, A.; Sciavicco, G., Propositional interval neighborhood temporal logics, Journal of Universal Computer Science, 9, 9, 1137-1167 (2003) |
| [11] | Goranko, V.; Montanari, A.; Sciavicco, G., A road map of interval temporal logics and duration calculi, Journal of Applied Non-Classical Logics, 14, 1-2, 9-54 (2004) · Zbl 1181.03012 |
| [12] | Goranko, V.; Montanari, A.; Sciavicco, G.; Sala, P., A general tableau method for propositional interval temporal logics: Theory and implementation, Journal of Applied Logic, 4, 3, 305-330 (2006) · Zbl 1104.03010 |
| [13] | Goranko, V.; Otto, M., Model theory of modal logic, (Blackburn, P.; etal., Handbook of Modal Logic (2007), Elsevier), 249-329 |
| [14] | Grädel, E.; Kolaitis, P. G.; Vardi, M. Y., On the decision problem for two-variable first-order logic, Bulletin of Symbolic Logic, 3, 1, 53-69 (1997) · Zbl 0873.03009 |
| [15] | Halpern, J.; Shoham, Y., A propositional modal logic of time intervals, Journal of the ACM, 38, 4, 935-962 (1991) · Zbl 0799.68175 |
| [16] | Immerman, N.; Kozen, D., Definability with bounded number of bound variables, Information and Computation, 83, 2, 121-139 (1989) · Zbl 0711.03004 |
| [17] | Kamp, H., Events, instants and temporal reference, (Bäuerle, R.; Egli, U.; Schwarze, C., Semantics from Different Points of View (1979), de Gruyter), 376-417 |
| [18] | Lodaya, K., Sharpening the undecidability of interval temporal logic, (Proc. of the 6th Asian Computing Science Conference. Proc. of the 6th Asian Computing Science Conference, ASIAN. Proc. of the 6th Asian Computing Science Conference. Proc. of the 6th Asian Computing Science Conference, ASIAN, LNCS, vol. 1961 (2000), Springer), 290-298 · Zbl 0987.03015 |
| [19] | Marx, M.; Reynolds, M., Undecidability of compass logic, Journal of Logic and Computation, 9, 6, 897-914 (1999) · Zbl 0941.03018 |
| [20] | Montanari, A.; Sciavicco, G.; Vitacolonna, N., Decidability of interval temporal logics over split-frames via granularity, (Proc. of the 8th European Conference on Logics in AI. Proc. of the 8th European Conference on Logics in AI, JELIA. Proc. of the 8th European Conference on Logics in AI. Proc. of the 8th European Conference on Logics in AI, JELIA, LNAI, vol. 2424 (2002), Springer), 259-270 · Zbl 1013.03013 |
| [21] | Mortimer, M., On languages with two variables, Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, 21, 135-140 (1975) · Zbl 0343.02009 |
| [22] | B. Moszkowski, Reasoning about digital circuits, Tech. Rep. STAN-CS-83-970, Dept. of Computer Science, Stanford University, Stanford, CA, 1983; B. Moszkowski, Reasoning about digital circuits, Tech. Rep. STAN-CS-83-970, Dept. of Computer Science, Stanford University, Stanford, CA, 1983 |
| [23] | Otto, M., Two variable first-order logic over ordered domains, Journal of Symbolic Logic, 66, 2, 685-702 (2001) · Zbl 0990.03005 |
| [24] | Scott, D., A decision method for validity of sentences in two variables, Journal of Symbolic Logic, 27-377 (1962) |
| [25] | Shapirovsky, I.; Shehtman, V., Chronological future modality in Minkowski spacetime, (Balbiani, P.; Suzuki, N. Y.; Wolter, F.; Zakharyaschev, M., Advances in Modal Logic, vol. 4 (2003), King’s College Publications: King’s College Publications London), 437-459 · Zbl 1082.03016 |
| [26] | Venema, Y., Expressiveness and completeness of an interval tense logic, Notre Dame Journal of Formal Logic, 31, 4, 529-547 (1990) · Zbl 0725.03006 |
| [27] | Venema, Y., A modal logic for chopping intervals, Journal of Logic and Computation, 1, 4, 453-476 (1991) · Zbl 0744.03022 |
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.
