L*n系统中α-反向FMP和α-反向FMT问题的解

摘要

提出了α-反向FMP、多重α-反向FMP,以及α-反向FMT和多重α-反向FMT问题.通过在F(S)中引入一个预序,在L*n系统中,给出了上述问题的解.并说明了这些解从形式上和α-反向三I算法的结果一致,从而在逻辑系统L*n中建立了反向三I算法的形式化推理机制.%It proposes problems of α-reverse FMP, collective α-reverse FMP, as well as α-reverse FMT, collective α-reverse FMT. By introducing a preorder in F(S) , the solutions for these problems are given in propositional logical sys-tem L*n . And it clarifies that these solutions can be brought into line with the solutions of methods of α-reverse triple-I. Therefore, formal reasoning system of α-reverse triple-Ⅰ problems is provided in propositional logical system L*n .