Page 129 - 《软件学报》2020年第12期

张玉志 等:面向完美回忆的时态认知逻辑 3795

n
知识库进行存储,认知状态会立即变成你在 2018 年 12 月 5 日知道 p(记为 K p ).在此之后的任何时间点上你都
a
知道 p,并且你都记得 K¬ n− a 2 , p ¬ K a n− 1 , pK pK a n+ 1 , pK a n+ 2 p ,... .
n
,
a
t
t
S5 C 系统的构建理念及其结论在人工智能、分布式系统、博弈论等领域具有潜在应用价值,如可以据此
探讨智能机器人的知识库扩充原则和方法,可以从模型上解释博弈中的主体(群体)如何根据自己认知状态的变
t
化历史而制定策略等.鉴于时态逻辑在人工智能、软件工程、规划问题和信息安全等领域有着广泛应用,在 S5 C t
t
t
系统的基础上考虑兼顾更多时序方面的性质,或许是未来一项有意义的工作.另外,S5 C 系统的公式中存在时间
点,在模型上可以在不同的时间点上任意跳跃,这与混合逻辑(hybrid logic)的一些思想存在共性.利用混合逻辑
的技术,完全可以在语形上达到准确刻画主体认知状态的效果.例如,文中公理 Ax5 完全可以利用混合逻辑的技
术表述为“@ m K a ϕ→@ n K a ϕ,m<n”.但是,加入混合逻辑的技术后给出一套合适的模型会成为一个新的难题.我们
认为,这也是未来值得进一步研究的方向之一.
References:
[1] Sato M. A study of kripke-type models for some modal logics by gentzen's sequential method [Ph.D. Thesis]. University of Kyoto,
1977.
[2] Lehmann D. Knowledge, common knowledge, and related puzzles (extended summary). In: Proc. of the 3rd Annual ACM Symp. on
Principles of Distributed Computing. 1984. 62−67. [doi: 10.1145/800222.806736]
[3] Parikh R, Ramanujam R. Distributed processes and the logic of knowledge. In: Proc. of the Logic of Programs Conf. Springer-
Verlag, 1985. 256−268. [doi: 10.1007/3-540-15648-8_21]
[4] Kraus S, Lehmann D. Knowledge, belief and time. Theoretical Computer Science, 1988,58(1-3):155−174. [doi: 10.1016/0304-
3975(88)90024-2]
[5] Halpern JY, Vardi MY. The complexity of reasoning about knowledge and time. i. lower bounds. Journal of Computer and System
Sciences, 1989,38(1):195−237. [doi: 10.1016/0022-0000(89)90039-1]
[6] Spaan E. Nexttime is not necessary. In: Proc. of the Theoretical Aspects of Reasoning about Knowledge Conf. Morgan Kaufmann
Publishers Inc., 1990. 241−256.
[7] Meyden RVD. Axioms for knowledge and time in distributed systems with perfect recall. In: Proc. of the 9th Annual IEEE Symp.
on Logic in Computer Science. 1994. 448−457.
[8] Ditmarsch HV, Halpern JY, Hoek WVD, Kooi B. Handbook of Epistemic Logic. College Publications, 2015. 395−442.
[9] Halpern JY, Vardi MY. Model checking vs. theorem proving: A manifesto. Artificial Intelligence and Mathematical Theory of
Computation, 1991,212:151−176. [doi: 10.1016/B978-0-12-450010-5.50015-3]
[10] Meyden RVD, Shilov NV. Model checking knowledge and time in systems with perfect recall. In: Proc. of the Foundations of
Software Technology and Theoretical Computer Science. 1999. 432−445. [doi: 10.1007/3-540-46691-6_35]
[11] Hoek WVD, Wooldridge M. Model checking knowledge and time. In: Proc. of the Int’l Spin Workshop on Model Checking of
Software. 2002. 95−111. [doi: 10.1007/3-540-46017-9_9]
[12] Wu LJ, Su KL. A model checking algorithm for temporal logics of knowledge in multi-agent systems. Ruan Jian Xue Bao/Journal
of Software, 2004,15(7):1012−1020 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/15/1012.htm
[13] Luo XY, Su KL, Yang JJ. Bounded model checking for temporal epistemic logic in synchronous multi-agent systems. Ruan Jian
Xue Bao/Journal of Software, 2006,17(12):2485−2498 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/17/
2485.htm
[14] Luo XY, Su KL, Gu M. A model checking approach for solving epistemic riddles. Chinese Journal of Computers, 2010,33(3):
406−414 (in Chinese with English abstract).
[15] Frege G, Wrote; Wang L, Trans. Anthology of Frege’s Philosophical Works. Beijing: Commercial Press, 2006. 128 (in Chinese).
[16] Haack S, Wrote; Luo Y, Trans. Philosophy of Logics. Beijing: Commercial Press, 2003. 193−200 (in Chinese).
[17] Fagin R, Halpern JY, Moses Y, Vardi MY. Reasoning About Knowledge. MIT Press, 1995.
[18] Ditmarsch HV, Hoek WVD, Kooi B. Dynamic Epistemic Logic. Springer Press, 2007.