Logic for Computer Scientists
By 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.
12 Equivalence and Normal Forms
13 Horn Formulas
14 The Compactness Theorem
22 Normal Forms
26 Refinements of Resolution
32 Horn Clause Programs
33 Evaluation Strategies
Table of Notations
24 Herbrands Theory
Other editions - View all
algorithm arity assignment atomic formulas Automated Theorem Proving axiomatizable called clause from F clause in F clause set F closed formula compactness theorem conﬁguration consequence of F contain deﬁned deﬁnition empty clause evaluation strategy example Exercise exists F is unsatisﬁable F V G ﬁnite ﬁrst form F formula F formula in DNF formulas in predicate function symbols goal clause ground instance Herbrand structure Horn clauses Horn formulas induction hypothesis inﬁnite Let F linear resolution logic program model for F obtain occurring in F predicate logic predicate symbols prenex form procedure program clause program F programming language PROLOG propositional logic resolution is complete resolution proof resolution refutation resolution restrictions resolution step resolvent satisﬁable Section 2.3 semantics semi-decision procedure sequence set of formulas Show Skolem form SLD-resolution subformula successful computation tautology theory truth value truth-table type 2 nondeterminism undecidable uniﬁer unsatisﬁable clause set unsatisﬁable formula variables