|
|||||
|
|
| 相关逻辑L5系统的Curry性质 | |
| 引用本文： | 刘叙华,孙吉贵.相关逻辑L5系统的Curry性质[J].中国科学A辑,1993,36(12):1320-1325. |
| 作者姓名： | 刘叙华 孙吉贵 |
| 作者单位： | 吉林大学计算机科学系 长春 130023 |
| 摘 要： | 本文改进了Thistlewaite, MoRobbie和Meyer的结果,证明了在命题相关逻辑LR的Gentzen型形式系统L5中,若多重集α是L5-可证的,则存在α的L5-证明τ具有Curry性质,从而简化了L5可判定性的证明。并指出:在具体的机器实现中使用Curry性质,提高了L5证明搜索的LR的自动定理证明的剪枝效率。 |
| 关 键 词： | 相关逻辑LR Curry性质 形式系统L5 自动定理证明 人工智能 |
| 点击此处可从《中国科学A辑》浏览原始摘要信息 | |
| 点击此处可从《中国科学A辑》下载免费的PDF全文 | |