摘要
本文改进了Thistlewaite, MoRobbie和Meyer的结果,证明了在命题相关逻辑LR的Gentzen型形式系统L_5中,若多重集α是L_5^-可证的,则存在α的L_5-证明τ具有Curry性质,从而简化了L_5可判定性的证明。并指出:在具体的机器实现中使用Curry性质,提高了L_5证明搜索的LR的自动定理证明的剪枝效率。
出处
《中国科学（A辑）》
CSCD
1993年第12期1320-1325,共6页
Science in China(Series A)
基金
国家自然科学基金
国家教育委员会博士点基金
国家攀登计划
"863"高科技计划资助项目
