Logic for Computer ScientistsBy the development of new fields and applications, such as Automated Theorem Proving and Logic Programming, Logic has obtained a new and important role in Computer Science. The traditional mathematical way of dealing with Logic is in some respect not tailored for Computer Science - plications. This book emphasizes such Computer Science aspects in Logic. It arose from a series of lectures in 1986 and 1987 on Computer Science Logic at the EWH University in Koblenz, Germany. The goal of this l- ture series was to give the undergraduate student an early and theoretically well-founded access to modern applications of Logic in Computer Science. A minimal mathematical basis is required, such as an understanding of the notation and knowledge about the basic mathematical proof techniques induction). More sophisticated mathematical kno- edge not a precondition read this book. Acquaintance with some conventional programming language, PASCAL, assumed. Several people helped in various ways in the preparation process of the original German version of this book: Johannes KSbler, Eveline and Rainer Schuler, and Hermann Engesser from B.I. Wissenschaftsverlag. Regarding the English version, I want to express my deep gratitude to Prof. Ronald Book. Without him, this translated version of the book would not have been possible. |
What people are saying - Write a review
We haven't found any reviews in the usual places.
Contents
PROPOSITIONAL LOGIC | 3 |
12 Equivalence and Normal Forms | 14 |
13 Horn Formulas | 23 |
14 The Compactness Theorem | 26 |
15 Resolution | 29 |
PREDICATE LOGIC | 41 |
22 Normal Forms | 51 |
23 Undecidability | 61 |
26 Refinements of Resolution | 96 |
LOGIC PROGRAMMING | 109 |
32 Horn Clause Programs | 117 |
33 Evaluation Strategies | 131 |
34 PROLOG | 141 |
155 | |
Table of Notations | 161 |
163 | |
Other editions - View all
Common terms and phrases
able algorithm allows answer applied arbitrary assignment assume atomic formulas called clause in F clause set closed complete computation Consider consists construct contain defined definition derivation element empty clause equivalent example Exercise exists express F is unsatisfiable finite first formally formula F function symbols further given gives goal clause ground instance Hence Herbrand Horn clauses Horn formulas induction infinite input interpretation leads Lemma Let F literal logic program marked means Observe obtain output positive possible predicate logic predicate symbols prenex form presentation problem procedure produce program clause PROLOG proof propositional logic Prove quantifiers question resolution step resolvent restriction result satisfiable semantics sequence Show situation SLD-resolution solution structure subformula subset substitution suitable Suppose theorem theory transformed tree truth undecidable unifier universe unsatisfiable valid variables Wine write