吉林大学学报(工学版) ›› 2016, Vol. 46 ›› Issue (6): 2021-2026.doi: 10.13229/j.cnki.jdxbgxb201606035

Previous Articles     Next Articles

Expressive power of decidable subclasses of open proxcheme

ZHANG Wei1, LIU Yu-hui2   

  1. 1.College of Computer Science and Engineering, Northeastern University, Shenyang 110819, China;
    2.Research Academy, Northeastern University, Shenyang 110819, China
  • Received:2015-07-02 Online:2016-11-20 Published:2016-11-20

PDF (PC)

194

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 FO2 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 FO2. 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

CLC Number: 

  • TP181
[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.
[1] DONG Sa, LIU Da-you, OUYANG Ruo-chuan, ZHU Yun-gang, LI Li-na. Logistic regression classification in networked data with heterophily based on second-order Markov assumption [J]. Journal of Jilin University(Engineering and Technology Edition), 2018, 48(5): 1571-1577.
[2] GU Hai-jun, TIAN Ya-qian, CUI Ying. Intelligent interactive agent for home service [J]. Journal of Jilin University(Engineering and Technology Edition), 2018, 48(5): 1578-1585.
[3] WANG Xu, OUYANG Ji-hong, CHEN Gui-fen. Measurement of graph similarity based on vertical dimension sequence dynamic time warping method [J]. 吉林大学学报(工学版), 2018, 48(4): 1199-1205.
[4] ZHANG Hao, ZHAN Meng-ping, GUO Liu-xiang, LI Zhi, LIU Yuan-ning, ZHANG Chun-he, CHANG Hao-wu, WANG Zhi-qiang. Human exogenous plant miRNA cross-kingdom regulatory modeling based on high-throughout data [J]. 吉林大学学报(工学版), 2018, 48(4): 1206-1213.
[5] HUANG Lan, JI Lin-ying, YAO Gang, ZHAI Rui-feng, BAI Tian. Construction of disease-symptom semantic net for misdiagnosis prompt [J]. 吉林大学学报(工学版), 2018, 48(3): 859-865.
[6] LI Xiong-fei, FENG Ting-ting, LUO Shi, ZHANG Xiao-li. Automatic music composition algorithm based on recurrent neural network [J]. 吉林大学学报(工学版), 2018, 48(3): 866-873.
[7] LIU Jie, ZHANG Ping, GAO Wan-fu. Feature selection method based on conditional relevance [J]. 吉林大学学报(工学版), 2018, 48(3): 874-881.
[8] WANG Xu, OUYANG Ji-hong, CHEN Gui-fen. Heuristic algorithm of all common subsequences of multiple sequences for measuring multiple graphs similarity [J]. 吉林大学学报(工学版), 2018, 48(2): 526-532.
[9] YANG Xin, XIA Si-jun, LIU Dong-xue, FEI Shu-min, HU Yin-ji. Target tracking based on improved accelerated gradient under tracking-learning-detection framework [J]. 吉林大学学报(工学版), 2018, 48(2): 533-538.
[10] LIU Xue-juan, YUAN Jia-bin, XU Juan, DUAN Bo-jia. Quantum k-means algorithm [J]. 吉林大学学报(工学版), 2018, 48(2): 539-544.
[11] QU Hui-yan, ZHAO Wei, QIN Ai-hong. A fast collision detection algorithm based on optimization operator [J]. 吉林大学学报(工学版), 2017, 47(5): 1598-1603.
[12] LI Jia-fei, SUN Xiao-yu. Clustering method for uncertain data based on spectral decomposition [J]. 吉林大学学报(工学版), 2017, 47(5): 1604-1611.
[13] SHAO Ke-yong, CHEN Feng, WANG Ting-ting, WANG Ji-chi, ZHOU Li-peng. Full state based adaptive control of fractional order chaotic system without equilibrium point [J]. 吉林大学学报(工学版), 2017, 47(4): 1225-1230.
[14] WANG Sheng-sheng, WANG Chuang-feng, GU Fang-ming. Spatio-temporal reasoning for OPRA direction relation network [J]. 吉林大学学报(工学版), 2017, 47(4): 1238-1243.
[15] MA Miao, LI Yi-bin. Multi-level image sequences and convolutional neural networks based human action recognition method [J]. 吉林大学学报(工学版), 2017, 47(4): 1244-1252.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] LIU Song-shan, WANG Qing-nian, WANG Wei-hua, LIN Xin. Influence of inertial mass on damping and amplitude-frequency characteristic of regenerative suspension[J]. 吉林大学学报(工学版), 2013, 43(03): 557 -563 .
[2] WANG Tong-jian, CHEN Jin-shi, ZHAO Feng, ZHAO Qing-bo, LIU Xin-hui, YUAN Hua-shan. Mechanical-hydraulic co-simulation and experiment of full hydraulic steering systems[J]. 吉林大学学报(工学版), 2013, 43(03): 607 -612 .
[3] ZHANG Chun-qin, JIANG Gui-yan, WU Zheng-yan. Factors influencing motor vehicle travel departure time choice behavior[J]. 吉林大学学报(工学版), 2013, 43(03): 626 -632 .
[4] XIAO Rui, DENG Zong-cai, LAN Ming-zhang, SHEN Chen-liang. Experiment research on proportions of reactive powder concrete without silica fume[J]. 吉林大学学报(工学版), 2013, 43(03): 671 -676 .
[5] CHEN Si-guo, JIANG Xu, WANG Jian, LIU Yan-heng, DENG Wei-wen, DENG Jun-yi. Mashup of vehicular ad-hoc network and universal mobile telecommunications system[J]. 吉林大学学报(工学版), 2013, 43(03): 706 -710 .
[6] MENG Chao, SUN Zhi-xin, LIU San-min. Multiple execution paths for virus based on cloud computing[J]. 吉林大学学报(工学版), 2013, 43(03): 718 -726 .
[7] XIAN Shu, ZHENG Jin, LU Xing, ZHANG Shi-peng. Identification approach of P2P flow based on the content redistribution model[J]. 吉林大学学报(工学版), 2013, 43(03): 727 -733 .
[8] LYU Yuan-zhi, WANG Shi-gang, YU Jue-qiong, WANG Xiao-yu, LI Xue-song. Display characteristics of one-dimensional integral imaging in virtual mode based on lenticular lens array[J]. 吉林大学学报(工学版), 2013, 43(03): 753 -757 .
[9] WANG Dan, LI Yang, NIAN Gui-jun, WANG Ke. An inhomogeneity mask for spatial watermarking[J]. 吉林大学学报(工学版), 2013, 43(03): 771 -775 .
[10] FENG Lin-han, QIAN Zhi-hong, SHANG Ke-cheng, ZHU Shuang. Improved hidden node collision avoidance strategy based on IEEE802.15.4[J]. 吉林大学学报(工学版), 2013, 43(03): 776 -780 .
Copyright © Journal of Jilin University(Engineering and Technology Edition), All Rights Reserved.
Tel: +86-431-85095297　Fax: +86-431-85094074　E-mail: xbgxb@jlu.edu.cn
Powered by Beijing Magtech Co. Ltd