The Computer Journal Advance Access published online on February 27, 2007
The Computer Journal, doi:10.1093/comjnl/bxl069
| ||||||||||||||||||||||||||||||||||||||||||||||||||
R-Calculus: An Inference System for Belief Revision
State Key Laboratory of Software Development Environment, Beihang University, 100083 Beijing, P.R. China
* Corresponding author: liwei{at}nlsde.buaa.edu.cn
Received 15 June 2006; revised 8 October 2006
First-order languages have been introduced to describe beliefs formally and the concept of revision is defined for model as well as proof. A logical inference system named R-calculus is defined to derive all maximal contractions of a base of belief set for its given refutations. The R-calculus consists of the structural rules, an axiom, a cut rule and the rules for logical connectives and quantifiers. Some examples are given to demonstrate how to use the R-calculus. Furthermore, the properties reachability, soundness and completeness of the R-calculus are formally defined and proved.
Key Words: Belief revision necessary antecedent R-calculus R-refutation