高级检索

    R-演算中若干问题的研究

    Study on R-Calculus

    • 摘要: 李未教授提出了R-演算系统,它是形式理论的修正演算系统,是OPEN过程模式和GUINA过程模式的基础.R-演算在这2种过程模式中的核心作用是,当一个形式理论与事实产生矛盾时,找出矛盾的必要前提,从而获得一个协调的子理论.通过3种不同的方法细致刻画R-演算的基本概念“必要前提”,第1种方法来自R-演算,第2种方法基于极大协调子集与极小非协调子集的,最后一种方法是对于R-必要前提的归纳定义.通过比较这3种方法,指出各自的优缺点,并从第3种方法推演出一个可靠并且相对完全的系统.在比较这3种方法的同时,还细致地探讨了R-终止式的上下界以及极大协调子集的不可枚举性.其中极大协调的不可枚举性在一定程度上表明了不存在一种同时满足可靠并且完全的系统.

       

      Abstract: The R-calculus, proposed by professor Li Wei, is a revision calculus for formal theories. It plays a key role in OPEN and GUINA logic. It can be considered as a tool to cut out the prerequisites of contradiction when a theory conflicts with some facts, hence resulting in a consistent sub-theory. In order to give a purely syntactic calculus, we make a deep exploration of the concept “necessary prerequisite”, and characterize it in three different ways. Furthermore, R-terminated sets and the maximally consistent subsets are also studied. The first way is a logical consequence of original R-calculus. And the second one is based on maximally consistent subset. The third one is an inductive formalization of R-prerequisite. By comparing these ways, we claim that each way has its own advantages and disadvantages. We chose the last one as our approach to derive a sound and relatively complete calculus, namely R′, which could be a better system for original purpose. The lower bound and upper bound of R-terminated sets are proposed. And we prove that deriving maximally consistent subsets of contradiction is not only non-recursive but even not recursive enumerable, which indicates that any purely syntactic system are not able to be both sound and complete.

       

    /

    返回文章
    返回