## 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 |

Bibliography | 155 |

Table of Notations | 161 |

163 | |

### Other editions - View all

### Common terms and phrases

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