The R-Calculus and the Finite Injury Priority Method
Wei Li · Journal of Computers · 2017
The R-calculus is a Gentzen-type deduction system to deduce a consistent theory from a theory to be revised and a theory to revise.Because the semi-decidability of the deduction in the first-order logic, the R-calculus is semi-decidable.By using the limit lemma and finite injury priority method in recursion theory, we shall recursively construct a sequence of formula sets such that the limit of exists, say is provable in the R-calculus, and each formula in is enumerated in or extracted from only finitely often, where Θ is a maximal consistent set of by .Moreover, a Gentzen-type deduction is constructed to deduce the sequence by the deduction rules in which the deduction is recursive (decidable, computable).