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

作　　者：ZHANG Wei 

机构地区：[1]State Key Laboratory of Software Development Environment,Beihang University [2]College of Information Science and Engineering,Northeastern University

出　　处：《Science China(Information Sciences)》2015年第1期70-80,共11页中国科学（信息科学）（英文版）

基　　金：supported by State Key Laboratory of Software Development Environment Open Fund (Grant No. SKLSDE-2012KF-02);Key Construction Program of the National 985 Project (Grant No. 26311005)

摘　　要：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.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.

关 键 词：open logic DECIDABILITY maximal contraction R-calculus mechanical theorem proving 

分 类 号：O141[理学—数学]