A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog
A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog
复制标题
Prolog技术定理证明器：Prolog中的新阐述和实现
DOI：
10.1016/0304-3975(92)90168-f
复制
发表时间：
1990
期刊：
影响因子：
--
通讯作者：
M. Stickel
中科院分区：
文献类型：
--
作者：
M. Stickel
PROLOG技术定理证明器(PTTP)是对完全一阶谓词演算完备的PROLOG的扩展。它与PROLOG的不同之处在于，它使用了统一和出现的正确性检查，用深度优先迭代加深搜索代替无限深度优先搜索来完成搜索策略，以及在PROLOG推理中加入模型消元归约规则来完成推理系统。本文描述了一种新的基于Prolog的PTTP实现方法。它使用三种编译时转换将公式转换成PROLOG子句，在几个运行时谓词的支持下，直接执行深度优先迭代深化搜索和与发生检查统一的模型消除过程。它的高性能超过了基于PROLOG的PTTP解释器，并且比早期的基于LIP语言的编译器更简洁和可读性更好，这使得它在解释方面更优越。编译时转换的输入和输出示例提供了一种简单而准确的方法来解释PTTP如何工作。这个基于PROLOG的版本使得将PTTP定理证明思想融入到PROLOG程序中变得更容易。对扩展Prolog提出了一些建议，可用于提高PTTP的性能。
A Prolog technology theorem prover (PTTP) is an extension of Prolog that is complete for the full first-order predicate calculus. It differs from Prolog in its use of unification with the occurs check for soundness, depth-first iterative-deepening search instead of unbounded depth-first search to make the search strategy complete, and the model elimination reduction rule that is added to Prolog inferences to make the inference system complete. This paper describes a new Prolog-based implementation of PTTP. It uses three compile-time transformations to translate formulas into Prolog clauses that directly execute, with the support of a few run-time predicates, the model elimination procedure with depth-first iterative-deepening search and unification with the occurs check. Its high performance exceeds that of Prolog-based PTTP interpreters, and it is more concise and readable than the earlier Lisp-based compiler, which makes it superior for expository purposes. Examples of inputs and outputs of the compile-time transformations provide an easy and precise way to explain how PTTP works. This Prolog-based version makes it easier to incorporate PTTP theorem-proving ideas into Prolog programs. Some suggestions are made on extensions to Prolog that could be used to improve PTTP's performance.