A prolog technology theorem prover: Implementation by an extended prolog compiler
A prolog technology theorem prover: Implementation by an extended prolog compiler
复制标题
Prolog 技术定理证明器：扩展 Prolog 编译器的实现
DOI：
10.1007/bf00297245
复制
发表时间：
1986
期刊：
影响因子：
--
通讯作者：
M. Stickel
中科院分区：
文献类型：
--
作者：
M. Stickel
PROLOG技术定理证明器(PTTP)是对完全一阶谓词演算完备的PROLOG的扩展。它与PROLOG的不同之处在于，它使用了统一和出现的正确性检查，在PROLOG推理中加入模型消去约简规则来完成推理系统，并使用深度优先迭代加深搜索来代替无界深度优先搜索来完成搜索策略。一个PROLOG技术定理证明器已经由一个扩展的PROLOG到LISP编译器实现，该编译器支持这些附加功能。它能够以每秒数千次的速度证明完全一阶谓词演算中的定理。
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, the model-elimination reduction rule that is added to Prolog inferences to make the inference system complete, and depth-first iterative-deepening search instead of unbounded depthfirst search to make the search strategy complete. A Prolog technology theorem prover has been implemented by an extended Prolog-to-LISP compiler that supports these additional features. It is capable of proving theorems in the full first-order predicate calculus at a rate of thousands of inferences per second.