Implementation and Analysis of Proof Techniques Employing Negation Normal Form

这是一个计算逻辑的研究项目。研究领域直接源于对几个研究主题否定中公式结构的分析。在命题水平上的大量实验结果，在一阶水平上的初步实验结果，以及某些理论结果表明，其中最重要的可能是路径溶解，这是一种在基本水平上强完备的推理规则。对这一点和相关推理机制的探索将继续进行，主要是通过实验。调查的一个主要目的将是进一步实现先前开发的路径解析和语义图技术。一个复杂的地面系统和一个一阶系统现已投入使用；后者是一个坚实的平台，将在其上测试以下提议的技术：链接选择；计算主要蕴含；回溯；理论链接和解散；以及星链。虽然抽象的证明论问题本身是有意义的，但开发定理证明系统的性能增强也是一个主要动机。将对一些这样的改进进行调查。其中包括：提高现有推理机制的效率；利用现有机制改进证据搜索；以及开发新的推理技术来改变搜索空间本身。具体地说，系统开发将通过以下方面的研究来加强：溶解、分析表和分布规律；溶解与分解；量词重复、证明长度和循环；计算主要蕴涵的算法；以及归纳和相等。

This is a research project in computational logic. The areas of research stem directly from the analysis of the structure of formulas in negation toward several research topics. Substantial experimental results at the propositional level, preliminary experimental results at the first order level, and certain theoretical results indicate that the most important of these may be path dissolution, a rule of inference that is strongly complete at the ground level. Exploration of this and related inference mechanisms will be continued, largely through experimentation. One major thrust of the investigation will be to further the implementation of the path resolution and semantic graph techniques developed earlier. A sophisticated ground system and a first order system are now operational; the latter is a solid platform on which techniques proposed below will be tested: link selection; computing prime implicants; backtracking; theory links and dissolution; and star chains. While abstract proof-theoretic questions are of interest in their own right, the development of performance enhancements for the theorem proving system is also a major motivation. A number of such enhancements will be investigated. Among them are: improved efficiency of existing inference mechanisms; improved proof search with existing mechanisms; and development of new inference techniques that alter the search space itself. Specifically, system development will be enhanced through investigation of: dissolution, analytic tableaux, and the distributive law; dissolution versus resolution; quantifier duplication, proof length, and cycles; algorithms for computing prime implicants; and induction and equality.