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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
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