导读:本文包含了归结证明树论文开题报告文献综述、选题提纲参考文献，主要关键词:原理,程序。
邹伟松[1]（2002）在《从归结证明树抽取程序》一文中研究指出对于形如((?)x)((?)y)P(x，y)的定理证明问题，利用归结原理可以回答其是否为真，而对于“对每个确定的x，y的值是什么?”这一经典的证明论问题，归结原理则无能为力。有许多人研究从归结证明树确定y的值的方法。比较有代表性的是Green的方法和Luckham的方法。但由于他们的方法都不是从分析归结证明过程出发的，所以他们的方法存在许多局限性。 在这篇论文中，我们主要做了如下两项工作：第一，对于形如((?)x)((?)y)P(x，y)的定理证明问题，本文从分析归结证明树中的每个节点入手，提取归结证明的过程信息，生成一个程序。并且证明了抽取出的程序一定是部分正确的。这一方法的特点是，抽取算法的时间、空间复杂度都是线性的，并且抽取算法本身十分简单，易于实现。第二，对于形如((?)x)((?)y)((?)z)P(x，y，z)的定理证明问题，归结证明树中一定包含Skolem函数，而由这样的定理证明树中抽取出的程序就有可能包含Skolem函数。本文给出了是否能抽取出无Skolem函数的程序的充分必要条件，同时给出了抽取算法。(本文来源于《大连理工大学》期刊2002-03-01）
[1].邹伟松.从归结证明树抽取程序[D].大连理工大学.2002
本文来源: https://www.lunwen90.cn/article/6f9233e18486c4b712675eae.html