信念修正开放过程模式可判定公式表达能力

doi:10.13229/j.cnki.jdxbgxb201606035

摘要/Abstract

摘要： 提出了一种可以在两个极大可判定前缀词公式类上实现信念修正OPEN过程模式的算法,该算法从初始形式理论出发,依据不断获取的新事实信息,迭代修正形式理论,完成形式理论的进化。探讨了OPEN过程模式的两种可判定公式类的表达能力,证明了其表达能力强于一阶逻辑的子集FO²和模态逻辑,并给出了实际应用例子。

关键词: 人工智能, 信念修正, 开放过程模式, 可判定公式类, 表达能力, 定理机器证明

Abstract: An algorithm for OPEN proxcheme is proposed that functions in the two maximal decidable classes of first-order logic. The algorithm iteratively revises the formal theories according to new information and completes the evolution of the formal theories. The expressive power of the OPEN proxcheme is discussed. It is demonstrated that the OPEN proxcheme and R-calculus preserve the decidability of formulas in the two maximal decidable classes. Since the decision problem for modal logic and FO² can be transferred to that of the two maximal decidable classes, it can be concluded that the OPEN proxcheme and R-calculus are more expressive than the modal logic and FO². Practical examples, such as hardware description and verification, are provided.

Key words: artificial intelligence, belief revision, OPEN proxcheme, decidable logic formula classes, expressive power, mechanical theorem proving

中图分类号:

TP181

张伟, 柳玉辉. 信念修正开放过程模式可判定公式表达能力[J]. 吉林大学学报(工学版), 2016, 46(6): 2021-2026.

ZHANG Wei, LIU Yu-hui. Expressive power of decidable subclasses of open proxcheme[J]. 吉林大学学报(工学版), 2016, 46(6): 2021-2026.

参考文献

[1] Alchourron C E, Gardenfors R, Makinson D. On the logic of theory change: partial meet contraction and revision functions[J]. Journal of Symbolic Logic,1985,50(2):510-530.
[2] Li W. An open logic system[J]. Science China Series A,1992,35(10):1103-1113.
[3] Li W. Mathematical Logic—Foundations for Information Science[M]. Basel: Birkhauser Verlag, 2010:45-185.
[4] Benthem J. Reasoning and programming: analogies between logic and computation[C]∥Proceedings of the 1991 International Symposium on Logic Programming,San Diego, USA,1991:717-718.
[5] Benthem J. Dynamic logic for belief revision[J]. Journal of Applied Non-Classical Logics,2007,17(2):129-155.
[6] Darwiche A, Pearl J. On the logic of iterated belief revision[J]. Artificial Intelligence,1997,89(1/2):1-29.
[7] Nayak A, Goebel R, Orgun M. Iterated belief contraction from first principles[C]∥Proceedings of 20th International Joint Conference on Artificial Intelligence, Hyderabad, India, 2007:2568-2573.
[8] Fermé E, Hansson S O. AGM 25 years:twenty-five years of research in belief change[J]. Journal of Philosophical Logic, 2011,40(2):295-331.
[9] Li W. R-calculus: an inference system for belief revision[J]. Computer Journal,2007,50(4):378-390.
[10] Li W, Sui Y F, A sound and complete R-calculi with respect to contraction and minimal change[J]. Frontiers of Computer Science,2014,8(2):184-191.
[11] Zhang W. On the decidability of open logic[J]. Science China: Information Science, 2009,52(8):1283-1291.
[12] Li H, Luo J, Li W. A formal semantics for debugging synchronous message passing-based concurrent programs[J]. Science China: Information Science,2014,57:128101.
[13] Luan S M, Dai G Z, Li W. A programmable approach to revising knowledge base[J]. Science China:Information Science,2005,48(6):681-692.
[14] Luo J, Li W. An algorithm to compute maximal contractions for Horn clauses[J]. Science China: Information Science,2011,54(2):244-257.
[15] Zhang W. Decidable subsets of open logic and an algorithm for R-calculus[J]. Science China: Information Science,2015,58(1):012103.
[16] 刘磊,张银平. 一种基于描述逻辑的构件检索匹配算法[J]. 吉林大学学报:工学版,2008,38(3):671-675.
Liu Lei, Zhang Yin-ping. Component retrieval and matching algorithm based on description logics[J]. Journal of Jilin University(Engineering and Technology Edition),2008,38(3):671-675.
[17] 黄宏涛,王静,叶海智,等. 基于惰性切片的线性时态逻辑性质验证[J]. 吉林大学学报:工学版,2015,45(1):245-251.
Huang Hong-tao, Wang Jing, Ye Hai-zhi, et al. Lazy slicing based method for verifying linear temporal logic property[J]. Journal of Jilin University(Engineering and Technology Edition), 2015,45(1):245-251.
[18] 王生生,刘大有,吴瑕,等. 模糊空间描述逻辑及应用[J]. 吉林大学学报:工学版,2010,40(6):1634-1638.
Wang Sheng-sheng, Liu Da-you, Wu Xia, et al. Fuzzy spatial description logic and application[J]. Journal of Jilin University(Engineering and Technology Edition),2010,40(6): 1634-1638.
[19] Bärger E, Grädel E, Gurevich Y. The Classical Decision Problem[M]. Berlin: Springer, 2001:17-285.
[20] Gradel E, Kolaitis P, Vardi M. On the decision problem for two-variable first-order logic[J]. The Bulletin of Symbolic Logic,1997,3(1):53-69.
[21] Gradel E, Walukiewicz I. Guarded fixed point logic[C]∥Proceedings of 14th Symposium on Logic in Computer Science (LICS),Trento, Italy,1999:45-54.
[22] Gabbay D M. Expressive functional completeness intense logic[DB/OL]. [2015-06-23]. https://www.researchgate.net/publication/268658624_Expressive_Functional_Completeness_in_Tense_Logic_Preliminary_report.
[23] Scott D. A decision method for validity of sentences in two variables[J]. Journal of Symbolic Logic,1962,27(4):477-478.
[24] 张兴亮,郭立红,张传胜,等. CO 2 激光器高压脉冲触发系统的设计[J].中国光学,2012,5(4):416-422.
Zhang Xing-liang,Guo Li-hong, Zhang Chuan-sheng, et al. Design of high-voltage pulse trigger system for CO 2 laser[J]. Chinese Optics,2012,5(4):416-422.
[25] Etessami K, Vardi M Y, Wilke T. First-order logic with two variables and unary temporal logic[J]. Information and Computation,2002,179(2):279-295.
[26] 张旭霞,李斌,张黎明,等. 有机-无机复合纳米材料的传感应用及机理[J]. 中国光学,2015,8(4):651-666.
Zhang Xu-xia, Li Bin, Zhang Li-ming, et al. Sensing application and mechanism of organic-inorganic nanocomposites[J]. Chinese Optics,2015,8(4):651-666.

相关文章 15

[1]	董飒, 刘大有, 欧阳若川, 朱允刚, 李丽娜. 引入二阶马尔可夫假设的逻辑回归异质性网络分类方法[J]. 吉林大学学报(工学版), 2018, 48(5): 1571-1577.
[2]	顾海军, 田雅倩, 崔莹. 基于行为语言的智能交互代理[J]. 吉林大学学报(工学版), 2018, 48(5): 1578-1585.
[3]	王旭, 欧阳继红, 陈桂芬. 基于垂直维序列动态时间规整方法的图相似度度量[J]. 吉林大学学报(工学版), 2018, 48(4): 1199-1205.
[4]	张浩, 占萌苹, 郭刘香, 李誌, 刘元宁, 张春鹤, 常浩武, 王志强. 基于高通量数据的人体外源性植物miRNA跨界调控建模[J]. 吉林大学学报(工学版), 2018, 48(4): 1206-1213.
[5]	黄岚, 纪林影, 姚刚, 翟睿峰, 白天. 面向误诊提示的疾病-症状语义网构建[J]. 吉林大学学报(工学版), 2018, 48(3): 859-865.
[6]	李雄飞, 冯婷婷, 骆实, 张小利. 基于递归神经网络的自动作曲算法[J]. 吉林大学学报(工学版), 2018, 48(3): 866-873.
[7]	刘杰, 张平, 高万夫. 基于条件相关的特征选择方法[J]. 吉林大学学报(工学版), 2018, 48(3): 874-881.
[8]	王旭, 欧阳继红, 陈桂芬. 基于多重序列所有公共子序列的启发式算法度量多图的相似度[J]. 吉林大学学报(工学版), 2018, 48(2): 526-532.
[9]	杨欣, 夏斯军, 刘冬雪, 费树岷, 胡银记. 跟踪-学习-检测框架下改进加速梯度的目标跟踪[J]. 吉林大学学报(工学版), 2018, 48(2): 533-538.
[10]	刘雪娟, 袁家斌, 许娟, 段博佳. 量子k-means算法[J]. 吉林大学学报(工学版), 2018, 48(2): 539-544.
[11]	曲慧雁, 赵伟, 秦爱红. 基于优化算子的快速碰撞检测算法[J]. 吉林大学学报(工学版), 2017, 47(5): 1598-1603.
[12]	李嘉菲, 孙小玉. 基于谱分解的不确定数据聚类方法[J]. 吉林大学学报(工学版), 2017, 47(5): 1604-1611.
[13]	邵克勇, 陈丰, 王婷婷, 王季驰, 周立朋. 无平衡点分数阶混沌系统全状态自适应控制[J]. 吉林大学学报(工学版), 2017, 47(4): 1225-1230.
[14]	王生生, 王创峰, 谷方明. OPRA方向关系网络的时空推理[J]. 吉林大学学报(工学版), 2017, 47(4): 1238-1243.
[15]	马淼, 李贻斌. 基于多级图像序列和卷积神经网络的人体行为识别[J]. 吉林大学学报(工学版), 2017, 47(4): 1244-1252.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed