摘要
提出了α-反向FMP、多重α-反向FMP,以及α-反向FMT和多重α-反向FMT问题。通过在F（S）中引入一个预序,在Ln^＊系统中,给出了上述问题的解。并说明了这些解从形式上和α-反向三I算法的结果一致,从而在逻辑系统Ln^＊中建立了反向三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 system Ln^＊. 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-I problems is provided in propositional logical system Ln^＊.
出处
《计算机工程与应用》
CSCD
北大核心
2016年第11期26-29,共4页
Computer Engineering and Applications
基金
福建省教育厅科研项目(No.JB14218)
