R-calculus: An inference system for belief revision

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.