Temporal logic with accessibility temporal relations generated by time states themselves. (English) Zbl 1437.03081
Summary: We study a temporal logic with non-standard temporal accessibility relations. This logic is generated by semantic underground models, and any such a model has a base formed by a frame with temporal relations generated by temporal states themselves; potentially, any state possesses its own temporal accessibility relation, and it is possible that all of them can be different. We consider this to be the most plausible modelling, because any time state has, in principle, its own view on what is past (or future). Time relations may have non-empty overlaps and they can be totally intransitive. Thus, this approach may be suitable for analysis of the most general cases of reasoning about computation, information flows, reliability, and other areas of AI and CS. The main mathematical question under consideration here is the existence of algorithms for solving satisfiability problems. Here we solve this problem and find the required algorithms. In the final part of our paper we formulate some interesting open problems.
Keywords:
temporal logic; non-classical logics; information; knowledge representation; deciding algorithms; computability; information; satisfiability; decidabilityReferences:
| [1] | F. Baader, P. Marantidis, A. Mottet, A. Okhotin.Extensions of unificationmodulo ACUI,Mathematical Structures in Computer Science, (2019), 1-30. |
| [2] | F. Baader, P. Narendran,Unification of concept terms,Proceedings of the 11th International Workshop on Unification, UNIF-97, LIFO Technical Report, (2001), 97-98. · Zbl 0970.68166 |
| [3] | S.Babenyshev, V. Rybakov,Linear Temporal Logic LTL: Basis for Admissible Rules,J. Log. Comput.,21:2 (2011), 157-177. Zbl 1233.03026 · Zbl 1233.03026 |
| [4] | H. Friedman,One Hundred and Two Problems in Mathematical Logic,J. Symb. Log., 40(1975), 113-129. Zbl 0318.02002 · Zbl 0318.02002 |
| [5] | D.M. Gabbay, I.M. Hodkinson,An axiomatization of the temporal logic with until and since over the real numbers, J. Log. Comput.,1:2 (1990), 229-259. Zbl 0744.03018 · Zbl 0744.03018 |
| [6] | D.M. Gabbay, I.M. Hodkinson, M.A. Reynolds,Temporal Logic. Vol 1. Mathematical foundations and computational aspects, Clarendon Press, Oxford, (1994). Zbl 0921.03023 · Zbl 0921.03023 |
| [7] | R. Goldblatt,Logics of Time and Computations, CSLI Lecture Notes,7(1992), Chapter 6. MR1191162 |
| [8] | V. Goranko,Hierarchies of Modal and Temporal Logics with Reference Pointers, J. Log. Lang. Inf.,5:1 (1996), 1-24. Zbl 0851.03003 · Zbl 0851.03003 |
| [9] | S. Ghilardi,Unification in Intuitionistic Logic, J. Symb. Log.,64:2 (1999), 859-880. Zbl 0930.03009 · Zbl 0930.03009 |
| [10] | S. Ghilardi,Unification Through Projectivity, J. Log. Comput.,7:6 (1997), 733-752. Zbl 0894.08004 · Zbl 0894.08004 |
| [11] | S. Odintsov, V. Rybakov,Inference Rules in Nelson’s Logics, Admissibility and Weak Admissibility, Log. Univers.,9:1 (2015), 93-120. Zbl 1336.03036 · Zbl 1336.03036 |
| [12] | S. Odintsov, V. Rybakov,Unification and admissible rules for paraconsistent minimal Johanssons’ logic J and positive intuitionistic logicIPC+, Ann. Pure Appl. Logic, 164:7-8 (2013), 771-784. Zbl 1323.03029 · Zbl 1323.03029 |
| [13] | V.Rybakov,Refined common knowledge logics or logics of common information, Arch. Math. Log.,42:2 (2003), 179-200. Zbl 1030.03015 · Zbl 1030.03015 |
| [14] | V. Rybakov,Logical Consecutions in Discrete Linear Temporal Logic, J. Symb. Log., 70:4 (2005), 1137-1149. Zbl 1110.03010 · Zbl 1110.03010 |
| [15] | V. Rybakov,Linear temporal logic with until and next, logical consecutions, Ann. Pure Appl. Logic,155:1 (2008), 32-45. Zbl 1147.03008 · Zbl 1147.03008 |
| [16] | V. Rybakov,Logic of knowledge and discovery via interacting agents-Decision algorithm for true and satisfiable statements, Inf. Sci.,179:11 (2009), 1608-1614. Zbl 1179.68151 · Zbl 1179.68151 |
| [17] | V. Rybakov,Linear Temporal LogicLT LKextended by Multi-Agent LogicKnwith Interacting Agents, J. Log. Comput.,19:6 (2009), 989-1017. Zbl 1208.03023 · Zbl 1208.03023 |
| [18] | V. Rybakov,Logical Analysis for Chance Discovery in Multi-Agents’ Environment, KES 2012, Conference Proceedings, Springer, (2012), 1593-1601. |
| [19] | V. Rybakov,Writing out unifiers in linear temporal logic, J. Log. Comput.,22:5 (2012), 1199-1206. Zbl 1259.03029 · Zbl 1259.03029 |
| [20] | V.Rybakov,Non-transitive linear temporal logic and logical knowledge operations, J. Log. Comput.,26:3 (2016), 945-958. Zbl 1403.03028 · Zbl 1403.03028 |
| [21] | V.V. Rybakov,Nontransitive temporal multiagent logic, information and knowledge, deciding algorithms, Sib. Math. J.,58:5 (2017), 875-886. Zbl 1420.03060 · Zbl 1420.03060 |
| [22] | V. Rybakov,Multiagent temporal logics with multivaluations, Sib. Math. J.,59:4 (2018), 710-720. Zbl 06976648 · Zbl 1469.03047 |
| [23] | V. Rybakov,Linear Temporal Logic with Non-transitive Time, Algorithms for Decidability and Verification of Admissibility, inOutstanding Contributions to Logic, Springer, 2018, 219-243. Zbl 1429.03074 · Zbl 1429.03074 |
| [24] | V. Rybakov,Temporal multi-valued logic with lost worlds in the past, Sib. Electron. Math. Izv.,15(2018), 436-449. Zbl 06931667 · Zbl 1436.03154 |
| [25] | V. Rybakov,Branching time agents’ logic, satisfiability problem by rules in reduced form, Sib. Electron. Math. Izv.,16(2019), 1158-1170. Zbl 07122035 · Zbl 1436.03126 |
| [26] | R. Schmidt, D. Tishkovsky,Solving rule admissibility problem for S4 by a tableau method, Automated Reasoning Workshop, (2011), 30. |
| [27] | S. Babenyshev, V. Rybakov, R. Schmidt, D. Tishkovsky,A tableau method for checking rule admissibility in S4, Electronic Notes in Theoretical Computer Science,262(2010), 17-32. Zbl 1345.03033 · Zbl 1345.03033 |
| [28] | J. van Benthem,Tense logic and time, Notre Dame J. Formal Logic,25:1 (1984), 1-16. Zbl 0536.03008 · Zbl 0536.03008 |
| [29] | M.Vardi,Anautomata-theoreticapproachtolineartemporallogic, in:Y.BanffHigherOrderWorkshop(1995),238-266.Availableat http://citeseer.ist.psu.edu/vardi96automatatheoretic.html. · Zbl 1543.68236 |
| [30] | M. Vardi, Reasoning about the past with two-way automata, in: Larsen K.G.(ed.) et al., ICALP, LNCS,1443(1998), 628-641. Zbl 0909.03019 · Zbl 0909.03019 |
| [31] | Yde Venema,Temporal Logic,chapter in: Lou Goble (ed),The Blackwell Guide on Philosophical Logic, Blackwell Publishers, Oxford, 2001, 203-223. · Zbl 0997.03019 |
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.
