Decidable subsets of open logic and an algorithm for R-calculus

详细信息    查看全文

• 作者：Wei Zhang (1) (2)
  
  1. State Key Laboratory of Software Development Environment ; Beihang University ; Beijing ; 100191 ; China
  2. College of Information Science and Engineering ; Northeastern University ; Shenyang ; 110819 ; China
  
• 关键词：open logic ; decidability ; maximal contraction ; R ; calculus ; mechanical theorem proving ; 012103
• 刊名：SCIENCE CHINA Information Sciences
• 出版年：2015
• 出版时间：January 2015
• 年：2015
• 卷：58
• 期：1
• 页码：1-11
• 全文大小：234 KB
• 参考文献：1. Li W. An open logic system. Sci China Ser A, 1992, 36: 362鈥?75
  2. Li W. Mathematical Logic-Foundations for Information Science. Basel: Birkhauser Verlag, 2010. 45鈥?85
  3. Alchourron C E, Gardenfors R, Makinson D. On the logic of theory change: partial meet contraction and revision functions. J Symbolic Logic, 1985, 50: 510鈥?30 2307/2274239" target="_blank" title="It opens in new window">CrossRef
  4. Benthem J. Dynamic logic for belief revision. J Appl Non-Classical Logics, 2007, 17: 129鈥?55 29-155" target="_blank" title="It opens in new window">CrossRef
  5. Luo J, Li W. An algorithm to compute maximal contractions for Horn clauses. Sci China Inf Sci, 2011, 54: 244鈥?57 2-010-4172-9" target="_blank" title="It opens in new window">CrossRef
  6. Luo J, Li W. R-calculus without the cut rule. Sci China Inf Sci, 2011, 54: 2530鈥?543 2-011-4492-4" target="_blank" title="It opens in new window">CrossRef
  7. Luan S M, Dai G Z, Li W. A programmable approach to revising knowledge base. Sci China Ser F-Inf Sci, 2005, 48: 681鈥?92 27" target="_blank" title="It opens in new window">CrossRef
  8. Boutilier C. Revision sequences and nested conditionals. In: Proceedings of 13th International Joint Conference on Artificial Intelligence, San Francisco, 1993. 519鈥?25
  9. Darwiche A, Pearl J. On the logic of iterated belief revision. Artif Intell, 1997, 89: 1鈥?9 2(96)00038-0" target="_blank" title="It opens in new window">CrossRef
  10. Nayak A, Goebel R, Orgun M. Iterated belief contraction from first principles. In: Proceedings of 20th International Joint Conference on Artificial Intelligence, San Francisco, 2007. 2568鈥?573
  11. Ma S, Sui Y, Xu K. The limits of Horn logic programs. In: Proceedings of 18th International Conference on Logic Programming, Denmark, 2002. 467鈥?78
  12. Su K, Li W. Computation of extensions of seminormal default theories. Fund Inform, 1999, 40: 79鈥?02
  13. Li W. R-calculus: an inference system for belief revision. Comput J, 2007, 50: 378鈥?90 CrossRef
  14. Li W, Zhang Y. An abstract logic for epistemic processes description (in Chinese). Sci China Ser E, 1996, 26: 168鈥?78
  15. Zhang W. On the decidability of open logic. Sci China Ser F-Inf Sci, 2009, 52: 1283鈥?291 2-009-0138-1" target="_blank" title="It opens in new window">CrossRef
  16. Li W, Luan S. A complete and operational approach to belief revision (in Chinese). J Software, 2002, 13: 59鈥?4
  17. B枚rger E, Gr盲del E, Gurevich Y. The Classical Decision Problem. Berlin: Springer-Verlag, 2001
  18. Wang H. Popular Lectures on Mathematical Logic. New York: Dover Publications Inc., 1993
  19. Kahr A, Moore E, Wang H. Entscheidungsproblem reduced to AEA case. In: Proceedings of the National Academy of Sciences of the United States of America, Washington, 1962. 365鈥?77
  20. Boas P. The Convenience of Tilings. In: Sorbi A, eds. Complexity, Logic, and Recursion Theory, Volume 187 of Lecture Notes in Pure and Applied Mathematics. New York: Marcel Dekker Inc, 1997. 331鈥?63
  21. Buchi R. Turing-machines and the entscheidungsproblem. Math Annalen, 1962, 148: 201鈥?13 CrossRef
  22. Gradel E. Dominoes and the complexity of subclasses of logical theories. Ann Pure Appl Logic, 1989, 43: 1鈥?0 2(89)90023-7" target="_blank" title="It opens in new window">CrossRef
  23. Zhu W, Xiao X. Introduction to Set Theory (in Chinese). Nanjing: Nanjing University Press, 1991. 87鈥?26
  
• 刊物类别：Computer Science
• 刊物主题：Chinese Library of Science
  Information Systems and Communication Service
  
• 出版者：Science China Press, co-published with Springer
• ISSN：1869-1919

文摘

Open logic is an attractive logic theory that can describe the growth and evolution of knowledge. However, related studies show that open logic is undecidable in first-order logic and thus is hard to be programmed. This paper proposes that open logic should be implemented with constraints, and provides a set of syntax constraints under which open logic is decidable. Furthermore, it is shown that the constraints are necessary and sufficient for the decidable formulas of open logic. A Domino problem-based algorithm R-CP that implements the R-calculus of the constrained open logic is presented and its reachability is proved.