Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Alchourrön C E, G→denfors R, Makinson D. On the logic of theory change: partial meet contraction and revision functions. J Symb Logic, 1985, 50: 510–530
Li W. A logical framework for evolution of specifications. In: Proceedings of 5th European Symposium on Programming, Edinburgh, UK, 1994. 394–408
Li W. Logical verification of scientific discovery. Sci China Inf Sci, 2010, 53: 677–684
Li W. R-calculus: an inference system for belief revision. Comput J, 2007, 50: 378–390
Li W. Mathematical Logic—Foundations for Information Science. Basel: Birkhäuser Verlag, 2010
Gallier J H. Logic for Computer Science: Foundations of Automatic Theorem Proving. New York: Harper & Row, 1986
Coq. http://coq.inria.fr/
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Luo, J., Li, W. R-calculus without the cut rule. Sci. China Inf. Sci. 54, 2530–2543 (2011). https://doi.org/10.1007/s11432-011-4492-4
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11432-011-4492-4