R-calculus without the cut rule  

作　　者：LUO Jie LI Wei 

机构地区：[1]State Key Laboratory of Software Development Environment, School of Computer Science and Engineering, Beihang University, Beijing 100191, China

出　　处：《Science China(Information Sciences)》2011年第12期2530-2543,共14页中国科学（信息科学）（英文版）

基　　金：supported by the National Basic Research Program of China(Grant No.2005CB321901);the National High Technology Research and Development Program of China(Grant No.2007AA01Z146);the State Key Laboratory of Software Development Environment Supported Project(Grant No.SKLSDE-2008ZX-01)

摘　　要：R-calculus is an inference system for deducing all possible changes when a theory is refuted by the facts. In this paper, we try to eliminate the cut rule in R-calculus by modifying the existing rules and by introducing new rules. The result is the R-calculus without the cut rule, which still preserves the reachability, soundness and completeness as R-calculus does. R-calculus without the cut rule is a formal inference system of logical connective symbols and quantifier symbols solely. It can serve as the theoretical foundation of the automation of revision calculus.

关 键 词：REVISION R-calculus cut rule 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程] O1-0[自动化与计算机技术—控制科学与工程]