From logic to logic programming
From logic to logic programming
复制标题
从逻辑到逻辑编程
DOI：
--
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
K. Doets
中科院分区：
文献类型：
--
作者：
K. Doets
来自出版商：
这本以数学为导向的逻辑规划理论介绍系统地阐述了命题逻辑、一阶逻辑和霍恩子句逻辑的解析方法，并分析了该方法的语义方面。正是通过解决的推理规则，证明和计算都可以在计算机上操作，本书包含逻辑编程证明理论中基本定理和引理的优雅版本和证明。涵盖了递归复杂性和否定失败及其语义等高级主题，并描述了 SLD 和 SLDNF 解析的简化设置。
没有其他书能如此详细和复杂地处理这些材料。 Doets 提供了一种新颖的解决方法，适用于一阶情况和（正）逻辑程序的情况。与通常的方法相反，解决方案的概念是非构造性定义的，不求助于统一的概念，允许以更经济的方式进行健全性和完整性证明。其他新材料包括处理分析层次结构的可计算性结果、无限推导的结果以及使用三值逻辑的一般逻辑程序的阐述。
From the Publisher:
This mathematically oriented introduction to the theory of logic programming presents a systematic exposition of the resolution method for propositional, first-order, and Horn- clause logics, together with an analysis of the semantic aspects of the method. It is through the inference rule of resolution that both proofs and computations can be manipulated on computers, and this book contains elegant versions and proofs of the fundamental theorems and lemmas in the proof theory of logic programming. Advanced topics such as recursive complexity and negation as failure and its semantics are covered, and streamlined setups for SLD- and SLDNF-resolution are described.
No other book treats this material in such detail and with such sophistication. Doets provides a novel approach to resolution that is applied to the first-order case and the case of (positive) logic programs. In contrast to the usual approach, the concept of a resolvent is defined nonconstructively, without recourse to the concept of unification, allowing the soundness and completeness proofs to be carried out in a more economic way. Other new material includes computability results dealing with analytical hierarchy, results on infinite derivations and an exposition on general logic programs using 3-valued logic.