From logic to logic programming
著者
書誌事項
From logic to logic programming
（MIT Press series in the foundations of computing）
MIT Press, c1994
大学図書館所蔵 全43件
注記
Includes bibliographical references (p. [197]-199) and index
内容説明・目次
内容説明
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.
目次
- Preliminaries - mathematical induction, trees, multisets, ordinals and cardinals
- propositional logic - syntax, semantics, conjunctive normal form, resolution
- first-order logic - syntax, semantics, quantifier-free sentences, universal sentences, Prenex and Skolem forms, resolution - the unrestricted version, unification, resolution
- program-definability - programs, the least Herbrand model, fixed points, hierarchies, definability, representing domains as Herbrand universes
- linear resolution - preliminaries, unrestricted linear resolution, ground completeness, linear resolution, SLD-resolution
- infinite derivations - negative information, non-standard algebras, resolution over non-standard algebras, realization trees, the interplay of SLD-trees and realization trees
- computability - preliminaries, computability of recursive functions, complexity of Tp
- negation - negation implemented - SLDNF, 3-valued models, 3-valued consequence operator, soundness, saturation, completeness for SLDNF.
「Nielsen BookData」 より