数理逻辑的经典书籍，目前并木有中译版，各位同学乘机刷一下英语吧Modern birkhauser classicsMany of the original research and survey monographs in pure andapplied mathematics published by Birkhauser in recent decadeshave been groundbreaking and have come to be regarded as foun-dational to the subject. Through the MBC Series, a select number ofthese modern classics, entirely uncorrected, are being re-released inpaperback (and as ebooks)to ensure that these treasures remain accessible to new generations of students, scholars, and researchersLogic forComputer ScientistsUwe SchoningReprint of the 1989 EditionBirkhauserBoston· Basel· BerlinUwe SchoningAbt. Theoretische InformatikUniversitat ulrOberer EselsbergD-89069UlmGEnglish hardcover edition originally published as volume 8 in the seriesProgress in Computer Science and Applied logic.German edition was published in 1987 as Logik far Informatiker byWissenschaftsverlag, Mannheim· Vienna· ZurichISBN-13:978-0-8176-47629e-ISBN-13:978-0-8176-4763-6DOI:10.1007978-0-8176-4763-6Library of Congress Control Number: 2007940259C2008 Birkhauser BostonAll rights reserved. This work may not be translated or copied in whole or in part without the written permission of the publisher(Birkhauser Boston, clo Springer Science+Business Media LLC, 233Spring Street, New York, NY 10013, USA), except for brief excerpts in connection with reviews orscholarly analysis. Use in connection with any form of information storage and retrieval, electronicadaptation, computer software, or by similar or dissimilar methodology now known or hereafter deThe use in this publication of trade names, trademarks, service marks and similar terms, even if theyare not identified as such, is not to be taken as an expression of opinion as to whether or not they aresubject to proprietary rightsCover design by Alex GerasevPrinted on acid-free paper987654321www.birkhausercomUwe SchoningLogic forComputer ScientistsWith 34 Illustrations1989BirkhauserBoston· Basel· BerlinUwe SchoningAbt. Theoretische InformatikUniversitat UlmOberer EselsbergD-89069UlmGermanyLibrary of Congress Cataloging- in-Publication DataSchoning, Uwe, 1955-Logic for computer scientists /Uwe Schoningp. cm.-( Progress in computer science and applied logicIncludes bibliographical referencesIsBn 0-8176-3453-0(alk. paper)Logic, Symbolic and mathematical 2. LLogic programmingI. TitleQA9S363198989-17864511.3-dc20CIPLogic for Computer Scientists was originally published in 1987as Logik fair Informatiker by Wissenschaftsverlag, Mannheim. Vienna. ZurichPrinted on acid-free paperC1989 Birkhauser BostonBirkhauserThird printing 1999All rights reserved. This work may not be translated or copied in whole or in part without the writtenpermission of the publisher(Birkhauser Boston, c/o Springer-Verlag New York, Inc, 175 Fifth AvenueNew York, NY 10010, USA), except for brief excerpts in connection with reviews or scholarly analysiUse in connection with any form of information storage and retrieval, electronic adaptation, computersoftware, or by similar or dissimilar methodology now known or hereafter developed is forbiddenThe use of general descriptive names, trade names, trademarks, etc, in this publication, even if the formerare not especially identified, is not to be taken as a sign that such names, as understood by the trade marksand Merchandise Marks Act, may accordingly be used freely by anyoneISBN0-81763453-3ISBN3-7643-3453-3Typeset by the author using LATEXPrinted and bound by Quinn-Woodbine, Woodbine, NJPrinted in the United States of America9876543Wolfram Schwabhausen(1931-1985)an grateful memoryPrefaceBy the development of new fields and application, such as AutomatedTheorem Proving and Logic Programming, Logic has obtained a new andimportant role in Computer Science. The traditional mathematical way ofdealing with Logic is in some respect not tailored for Computer Science ap.plications. This book emphasizes such Computer Science aspects in LogicIt arose from a series of lectures in 1986 and 1987 on Computer ScienceLogic at the EWH University in Koblenz, Germany. The goal of this lecture series was to give the undergraduate student an early and theoreticallywell-founded access to modern applications of Logic in Computer ScienceA minimal mathematical basis is required, such as an understandingof the set theoretic notation and knowledge about the basic mathematicalproof techniques(like induction). More sophisticated mathematical knowl-edge is not a precondition to read this book. Acquaintance with someconventional programming language, like PASCAL, is assumedSeveral people helped in various ways in the preparation process of theoriginal German version of this book: Johannes Kobler, Eveline and RainerSchuler, and Hermann Engesser from B I WissenschaftsverlagRegarding the English version, I want to express my deep gratitude toProf. Ronald Book. Without him, this translated version of the book wouldnot have been possibleKoblenz, June 1989U. SchoningContentsIntroduction1 PROPOSITIONAL LOGIC31.1 Foundations1.2 Equivalence and normal forms141.3 horn formulas,,,,,,,,,231.4 The Compactness Theorem261.5 Resolution292 PREDICATE LOGIC412.1 Foundations412.2 Normal Forms512.3 Undecidability2.4 Herbrand's Theory702.5 Resolut782.6 Refinements of resolution963 LOGIC PROGRAMMING1093.1 Answer Generation,1093.2 Horn Clause Programs1173.3 Evaluation Strategie1313.4 PROLOG141Bibliography155Table of notations161Index163