The AGM postulates are for the belief revision (revision by a single belief), and the DP postulates for the iterated revision (revision by a finite sequence of beliefs). Li gave an R-calculus for R-configurations Δ|Γ, where Δ is a set of atomic formulas or the negations of atomic formulas, and Γ is a finite set of formulas. In this paper, two deduction systems for the revision of a theory by another theory are given such that the systems are sound and complete, that is, if Δ|Γ ⇒ Γ′ is provable then Γ′ ⊇ Δ is consistent and Γ′ - Δ is a maximal subset of Γ such that (Γ′ - Δ) ∪ Δ is consistent; and for any finite theories Δ and Γ, there is a finite theory Γ ′ such that Γ′ - Δ is a maximal subset of G such that (Γ′ - Δ) ∪ Δ is consistent, and Δ|Γ ⇒ Γ′ is provable. Moreover, if Δ|Γ ⇒ Γ′ is provable then Γ satisfies the AGM and the DP postulates.
