Skip to main content

1987 | Buch

Foundations of Logic Programming

verfasst von: John Wylie Lloyd

Verlag: Springer Berlin Heidelberg

Buchreihe : Symbolic Computation

insite
SUCHEN

Über dieses Buch

In the two and a half years since the frrst edition of this book was published, the field of logic programming has grown rapidly. Consequently, it seemed advisable to try to expand the subject matter covered in the first edition. The new material in the second edition has a strong database flavour, which reflects my own research interests over the last three years. However, despite the fact that the second edition has about 70% more material than the first edition, many worthwhile topic!! are still missing. I can only plead that the field is now too big to expect one author to cover everything. In the second edition, I discuss a larger class of programs than that discussed in the first edition. Related to this, I have also taken the opportunity to try to improve some of the earlier terminology. Firstly, I introduce "program statements", which are formulas of the form A+-W, where the head A is an atom and the body W is an arbitrary formula. A "program" is a finite set of program statements. There are various restrictions of this class. "Normal" programs are ones where the body of each program statement is a conjunction of literals. (The terminology "general", used in the first edition, is obviously now inappropriate).

Inhaltsverzeichnis

Frontmatter
Chapter 1. Preliminaries
Abstract
This chapter presents the basic concepts and results which are needed for the theoretical foundations of logic programming. After a brief introduction to logic programming, we discuss first order theories, interpretations and models, unification, and fixpoints.
John Wylie Lloyd
Chapter 2. Definite Programs
Abstract
This chapter is concerned with the declarative and procedural semantics of definite programs. First, we introduce the concept of the least Herbrand model of a definite program and prove various important properties of such models. Next, we define correct answers, which provide a declarative description of the desired output from a program and a goal. The procedural counterpart of a correct answer is a computed answer, which is defined using SLD-resolution. We prove that every computed answer is correct and that every correct answer is an instance of a computed answer. This establishes the soundness and completeness of SLD-resolution, that is, shows that SLD-resolution produces only and all correct answers. Other important results established are the independence of the computation rule and the fact that any computable function can be computed by a definite program. Two pragmatic aspects of PROLOG implementations are also discussed. These are the omission of the occur check from the unification algorithm and the control facility, cut.
John Wylie Lloyd
Chapter 3. Normal Programs
Abstract
In this chapter, we study various forms of negation. Since only positive information can be a logical consequence of a program, special rules are needed to deduce negative information. The most important of these rules are the closed world assumption and the negation as failure rule. This chapter introduces normal programs, which are programs for which the body of a program clause is a conjunction of literals. The major results of this chapter are soundness and completeness theorems for the negation as failure rule and SLDNF-resolution for normal programs.
John Wylie Lloyd
Chapter 4. Programs
Abstract
In this chapter, we study programs and goals. A program is a finite set of program statements, each of which has the form A←W, where the head A is an atom and the body W is an arbitrary first order formula. Similarly, a goal has the form ←W, where the body W is an arbitrary first order formula. We prove the soundness of the negation as failure rule and SLDNF-resolution for programs and goals. We also study an error diagnoser, which is declarative in the sense that the programmer need only know the intended interpretation of an incorrect program to use the diagnoser.
John Wylie Lloyd
Chapter 5. Deductive Databases
Abstract
This chapter provides a theoretical basis for deductive database systems. A deductive database consists of a finite number of database statements, which have the form A←W, where A is an atom and W is a typed first order formula. A query has the form ←W, where W is a typed first order formula. An integrity constraint is a closed, typed first order formula. Function symbols are allowed to appear in formulas. Such a deductive database system can be implemented using a PROLOG system. The main results of this chapter are the soundness and completeness of the query evaluation process, the soundness of the implementation of integrity constraints, and a simplification theorem for implementing integrity constraints.
John Wylie Lloyd
Chapter 6. Perpetual Processes
Abstract
A perpetual process is a definite program which does not terminate and yet is doing useful computation, in some sense. With the advent of PROLOG systems for concurrent applications [18], [93], [106], especially operating systems, more and more programs will be of this type. Unfortunately, the semantics for definite programs developed in chapter 2 do not apply to perpetual processes, simply because they do not terminate. In this chapter, starting from the pioneering work of Andreka, van Emden, Nemeti and Tiuryn [2], we discuss the basic results of a semantics for perpetual processes.
John Wylie Lloyd
Backmatter
Metadaten
Titel
Foundations of Logic Programming
verfasst von
John Wylie Lloyd
Copyright-Jahr
1987
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-83189-8
Print ISBN
978-3-642-83191-1
DOI
https://doi.org/10.1007/978-3-642-83189-8