Improved Destructive Extension Rule in Propositional Modal Logic S5 System
Destructive method has been used for ATP (automated theorem proving) in modal logic because of its high solving efficiency.We have already extended it making it applicable to in S5 system.In this paper, we will put forward a new basic theory to promote the efficiency of algorithm.We define the ψ clause set and determine its satisfiability with this new basic theory.The advantage of the new method is that the complexity of the solving ψ clause set is equivalent to the complexity of solving classical logic clause set with the same number of atoms.It avoids some information introduced by destructive method previously.The embodiment of the accelerating effect of this method is relatively obvious when the quantity of formulas is high, the proportion of ψ formula is high and the number of atoms in ψ formula is large.Later in this paper, we analyze the improvement of its efficiency from the angle of theory.
Destructive method ψ clause set theorem proving modal logic S5
Pei Huang YuTing Yang Xi Tan Yuan Gao
College of Computer Science and Technology, Jilin University, Changchun, 130012, China
国际会议
三亚
英文
38-42
2015-12-26（万方平台首次上网日期，不代表论文的发表时间）