基本信息
- 原书名：Logic for Applications
- 原出版社： Springer
编辑推荐
“本书无疑是计算机科学最富成效的入门教科书之一……我们强烈建议把它作为教科书……”——美国计算机协会自动机与可计算性理论专业组(SIGACT)
内容简介
作译者
Anil Nerode 康奈尔大学数学系的创始人和教授，于1956年在芝加哥大学获得博士学位。他的研究领域包括数理逻辑、自动机、可计算理论、混合系统等。除本书外，他还与其他人合著了《Effective Completeness Theorems for Modal Logic》、《Tableaux for Constructive Concurrent Dynamic Logic》、《Logic，Categories，Lambda Calculus》等书。.
Richard A．Shore 康奈尔大学数学教授，于1972年在麻省理工学院获得博士学位。他的研究领域包括数理逻辑、递归论、集合论等。...
Richard A．Shore 康奈尔大学数学教授，于1972年在麻省理工学院获得博士学位。他的研究领域包括数理逻辑、递归论、集合论等。...
目录
Preface
Introduction.
I Propositional Logic
1 Orders and Trees
2 Propositions. Connectives and Truth Tables
3 Truth Assignments and Valuations
4 Tableau Proofs In Propositional Calculus
5 Soundness and Completeness of Tableau Proofs
6 Deductions from Premises and Compactness
7 An Axiomatic Approach*
8 Resolution
9 Refining Resolution
10 Linear Resolution. Horn Clauses and PROLOG
II Predicate Logic
1 Predicates and Quantifiers
2 The Language: Terms and Formulas
3 Formation Trees. Structures and Lists
4 Semantics: Meaning and Truth
5 Interpretations of PROLOG Programs
6 Proofs: Complete Systematic Tableaux
Introduction.
I Propositional Logic
1 Orders and Trees
2 Propositions. Connectives and Truth Tables
3 Truth Assignments and Valuations
4 Tableau Proofs In Propositional Calculus
5 Soundness and Completeness of Tableau Proofs
6 Deductions from Premises and Compactness
7 An Axiomatic Approach*
8 Resolution
9 Refining Resolution
10 Linear Resolution. Horn Clauses and PROLOG
II Predicate Logic
1 Predicates and Quantifiers
2 The Language: Terms and Formulas
3 Formation Trees. Structures and Lists
4 Semantics: Meaning and Truth
5 Interpretations of PROLOG Programs
6 Proofs: Complete Systematic Tableaux
前言
In writing this book, our goal was to produce a text suitable for a first course in mathematical logic more attuned than the traditional textbooks to the recent dramatic growth in the applications of logic to computer science. Thus, our choice of topics has been heavily influenced by such applications. Of course, we cover the basic traditional topics: syntax, semantics, soundness, completeness and compactness as well as a few more advanced results such as the theorems of Skolem-Lowenheim and Herbrand. Much of our book, however, deals with other less traditional topics. ResolutiOn theorem proving plays a major role in our treatment of logic especially in its application to Logic Programming and PROLOC. We deal extensively with the mathematical foundations of all three of these subjects. In addition, we include two chapters on nonclassical logics -- modal and intuitionistic -- that are becoming increasingly important in computer science. We develop the basic material on the syntax and semantics (via Kripke frames) for each of these logics. In both cases, our approach to formal proofs, soundness and completeness uses modifications of the same tableau method introduced for classical logic. We indicate how it can easily be adapted to various other special types of modal logics. A number of more advanced topics (lncluding nonmonotonic logic) are also briefly introduced both in the nonclassical logic chapters and in the material on Logic Programming and PROLOG. .
The intended audience for this text consists of upper level undergraduate and beginning graduate students of mathematics or computer science. We assume a basic background in abstract reasoning as would be provided by any beginning course in algebra or theoretical computer science as well as the usual familiarity with informal mathematical notation and argument as would be used in any such course. Basic set-theoretic terminology for orderings and trees is given in the opening section 1.1.1. We also supply a systematic treatment of elementary set theory in Chapter VI. This material can be used as a reference as needed or covered as part of the course at either its beginning or end.
If taught as a course for advanced undergraduates, essentially all the material in Chapters I-III, together with a reasonable amount of programming in PROLOG, can be covered in one semester with three hours of lectures a week. When teaching it in this way, we have had (and recommend) an additional weekly section evoted to homework problems and programming instruction. Alternatively, the material on resolution theorem proving and Logic Programming can be replaced by the chapters on modal and intuitionistic logic to get a rather different course. For two quarters, one can simply add on one of the nonclassical logics to the first suggested semester course. We have deliberately made these two chapters entirely independent of one another so as to afford a choice. There is, however, much similarity in the developments and, if both are covered, the corresponding sections of the second chapter can be covered more quickly. At the graduate level, essentially the whole book can be covered in a semester.
The text develops propositional logic in its entirety before proceeding to predicate logic. However, depending on the background of the class and the predilections of the instructor, it is possible to combine the treatments. Indeed, for a graduate course or with students with some previous exposure to propositional logic and truth tables, this may well be better. To follow such a path, begin with 1.1-2 and then move on to II.1-4. If planning to introduce PROLOG and develop the foundations of Logic Programming, II.5 can be used to explain the syntax and semantics of PROLOG. To start the students on actual programming, an informal introduction to PROLOG implementation and programming can be continued in the recitation section (parts of 1.10 are relevant here). Of course, the theoretical underpinnings must wait for the formal development of resolution and unification. With or without the Logic Programming, it is now possible (based on the tableau approach) to prove the soundness and completeness theerems for predicate logic in II.6-7 and to continue through the proof of Herbrand's theorem in II.10. A Hilbert-style proof system is presented without proving any results in 1.7 and II.8.
The resolution-style proof system on which PROLOG is based is more intimately tied to its development in the propositional case, as the basic theorems are proven by using Herbrand's theorem to reduce predicate logic results to corresponding ones of propositional logic. Thus, it is necessary, if covering this material, to do the propositional case first. The sections needed for the treatment of PROLOG are 1.8, 1.10 and II.11-13. The refinements of resolution considered in 1.9 are strictly optional. While linear resolution (II.14) is highly relevant to PROLOG, the completeness theorem is one of the most difficult in the text. We have therefore provided in III.1 an alternate approach to the corresponding results for Horn logic and PROLOG that requires only the basic definitions of linear resolution (I.14.1-3).
A diagram of the logical dependencies between sections of the text (except for Chapter VI) is given on the facing page. Unless Indicated otherwise by an arrow, the order of dependency runs right to left. Dotted lines (as from the propositional to predicate sections for classical logic) indicate relevance but not strict logical dependence. We should note that the very first section, I.1, simply collects definitions and facts about orderings and trees that are needed at various points in the text. This material can be covered at the beginning or inserted as needed. In particular, Konig's lemma, 1.1.4, is not needed until the treatment of complete systematic tableaux in 1.4. Similarly, the material on set-theoretic procedures in Chapter VI (new in this edition) can be covered at any point. Only one section (§6) assumes a familiarity with predicate logic and that is simply to list a formal version of the axioms. In this chapter, §§1-5 and §7 contain the basic set theory needed for this book and most undergraduate courses. The remaining sections, §§8-11, develop the theory of infinite (and even uncountable) ordinals, cardinals and transfinite recursion including some versions of the axiom of choice. This material should suffice as a background in set theory for most graduate courses in mathematics and computer science but is not used in the rest of this book.
At various other points in the text, certain paragraphs or even whole sections that are not needed for the later material are marked as optional by an asterisk (*). They are also printed in smaller type and with wider margins to set them off from the main line of development. In addition, there are three important possible exceptions to the order indicated above; these are of particular relevance for those courses not including very much about PROLOG. ..
The first exception also needs a warning. Our basic approach to logic does not include a specialized equality predicate. Although no longer the common approach in texts on mathematical logic, this is the right way to develop the subject to do resolution theorem proving, Logic Programming and PROLOG. We have thus relegated to III.5 the analysis of equality, either as a special predicate with the privileged semantics of true equality and the corresponding logical axiom schemes, or as an ordinary one with the appropriate equality axioms added on to each system under consideration. It is, however, quite possible to cover the relevant material in III.5 up to III.5.3 and the proofs of the soundness and completeness theorems for equality interpretations described there immediately after II.7.
The second exception concerns 'the proof of Church's theorem on the undecidability of validity for predicate logic. In III.8 we present a proof designed to apply even to the fragment of predicate logic represented in PROLOG. In Exercise 3 of III.5, however, we indicate how the presentation can easily be modified to make no mention of PROLOG notation or procedures and so give a proof of Church's theorem which is accessible after II.7.
Finally, the introduction to nonmonotonic logic given in III.7 up to III.7.6 can also be read independently of the material on Logic Programming and PROLOG. The rest of III.7 consists of an analysis of the stable models of Logic Programming with negation in terms of nonmonotonic logic. Other, more self-contained, applications to graphs and partial orders are given in Exercises 8-9 of III.7.
We should point out that there is a considerable overlap in the basic material for the development of modal and intuitionistic logic in Chapters IV and V. Indeed, a single unified development is possible albeit at some expense to the ease of intelligibility. We have instead written these chapters so that either may be read independently of the other. For the readers who wish to delve into both topics, we supply a comparative guide to basic notions of classical, modal and intuitionistic logic in V.6. We try there to point out the similarities and differences between these logics.
We have included a variety of problems at the end of almost every section of the text including a fair number of programming problems in PROLOO that can be assigned either for theoretical analysis or actual implementation. In particular, there are series of problems based on a database consisting of the genealogical lists in the first few chapters of Chronicles. It is reproduced in Appendix B. (An electronic version is available. Send an email request to shore@math.cornell.edu.) We have included these problems to serve as paradigms for use with a similar database or to be appropriately modified to fit other situations. This is not, however, a text on PROLOG programming. When teaching this material, we always supplement it with one of the standard texts on PROLOG programming listed in the suggestions for further reading at the end of Chapter III. Nothing in the text is tied to a particular version of the PROLOG language; we use only standard syntax and discuss typical implementations. We have ourselves used various implementations and platforms. The printouts of program runs are from ARITY PROLOG running on a PC.
When we (infrequently) cite results from the current literature, we attribute them as usual. However, as this is a basic textbook, we have made no attempt to attribute the standard results of the subject to their discoverers, other than when at times we name theorems according to common usage. We have, however, supplied a brief history of logic in an appendix that should give the student a feel for the development of the subject. In addition, suggestions for further reading that might be useful for either students or teachers using this text are given at the end of each chapter. Finally, a fairly extensive bibliography of related material, arranged by subject, is given at the end of the book.
Portions of this book appeared in various formats over many years. Very early versions of the material on classical logic and set theory appeared in lecture notes by Nerode which were distributed for courses at Cornell years ago. Part of this material was also independently reworked by George Metakides and appeared as lecture notes in English with Nerode and in Greek as his lectures at the University of Patras. Nerode [1990, 4.2] and [1991, 4.4] contain preliminary versions of our treatment of intuitionistic and modal logic based on the tableau method which were presented in lectures at Montecatini Terme and Marktoberdorf in 1988 and 1989, respectively. Our approach to resolution was also influenced by courses on program verification given by Richard Platek at Cornell. More current versions of the material have been read and used over the past years by a number of teachers in both mathematics and computer science departments and we have benefited considerably from their comments and suggestions. We should mention Uri Abraham (Mathematics, Ben Gurion University, Israel), John Crossley (Mathematics and Computer Science, Monash University, Australia), Ward Henson (Mathematics, University of Illinois, Urbana), Nils Klarlund (Computer Science, University of Aarhus, Denmark), Dexter Kozen (Computer Science, Cotnell) ,George Metakides (University of Patras, Greece and Information Technologies Research, EEC) and Jacob Plotkin (Mathematics, Michigan State University). Perry Smith (Math. Reviews) suggested Theorem 1.4.11 of this edition and its proof. Bakhadyr Khussainov pointed out an error in the previous edition in the proof of Theorem V.2.20. Warren Ooldfarb (Philosophy, Harvard) helped us avoid a number of pitfalls in the historical appendix. Particularly extensive (and highly beneficial)comments were received from Wiktor Marek (Computer Science, University of Kentucky), George Odifreddi (Computer Science, University of Turin, Italy) and Robert Soare (Mathematics and Computer Science, University of Chicago) who used several versions of the text in their courses. We also owe a debt to our graduate students who have served as assistants for our logic courses over the past few years and have made many corrections and suggestions: Jennifer Davoren, Steven Kautz, James Lipton, Sherry Marcus and Duminda Wijesekera.
We gratefully acknowledge the financial support over the past few years of the NSF under grants DMS-g601048, DMS-8902797, DMS-9204308, DMS-9503503; the ARO under grants DAAG29-85-C-O018 and DAAL03-91-C-0027 through ACSyAM at the Mathematical Sciences Institute of Cornell University; and IBM for an equipment grant through Project Ezra at Cornell University. We would also like to thank Arletta Havlik and Graeme Bailey for their help with the TEXing of the original version of the text for the previous edition as well as Geraldine Brady, Jennifer Davoren, Nathaniel Miller, Robert Miinikel, George Odifreddi and David Solomon for their help in proofreading.
Finally, in appreciation of their continuing support, we dedicate this book to our wives, Sally and Naomi. ...
Cornell University Anll Nerode
Ithaca, NY Richard A. Shore
June 1996
The intended audience for this text consists of upper level undergraduate and beginning graduate students of mathematics or computer science. We assume a basic background in abstract reasoning as would be provided by any beginning course in algebra or theoretical computer science as well as the usual familiarity with informal mathematical notation and argument as would be used in any such course. Basic set-theoretic terminology for orderings and trees is given in the opening section 1.1.1. We also supply a systematic treatment of elementary set theory in Chapter VI. This material can be used as a reference as needed or covered as part of the course at either its beginning or end.
If taught as a course for advanced undergraduates, essentially all the material in Chapters I-III, together with a reasonable amount of programming in PROLOG, can be covered in one semester with three hours of lectures a week. When teaching it in this way, we have had (and recommend) an additional weekly section evoted to homework problems and programming instruction. Alternatively, the material on resolution theorem proving and Logic Programming can be replaced by the chapters on modal and intuitionistic logic to get a rather different course. For two quarters, one can simply add on one of the nonclassical logics to the first suggested semester course. We have deliberately made these two chapters entirely independent of one another so as to afford a choice. There is, however, much similarity in the developments and, if both are covered, the corresponding sections of the second chapter can be covered more quickly. At the graduate level, essentially the whole book can be covered in a semester.
The text develops propositional logic in its entirety before proceeding to predicate logic. However, depending on the background of the class and the predilections of the instructor, it is possible to combine the treatments. Indeed, for a graduate course or with students with some previous exposure to propositional logic and truth tables, this may well be better. To follow such a path, begin with 1.1-2 and then move on to II.1-4. If planning to introduce PROLOG and develop the foundations of Logic Programming, II.5 can be used to explain the syntax and semantics of PROLOG. To start the students on actual programming, an informal introduction to PROLOG implementation and programming can be continued in the recitation section (parts of 1.10 are relevant here). Of course, the theoretical underpinnings must wait for the formal development of resolution and unification. With or without the Logic Programming, it is now possible (based on the tableau approach) to prove the soundness and completeness theerems for predicate logic in II.6-7 and to continue through the proof of Herbrand's theorem in II.10. A Hilbert-style proof system is presented without proving any results in 1.7 and II.8.
The resolution-style proof system on which PROLOG is based is more intimately tied to its development in the propositional case, as the basic theorems are proven by using Herbrand's theorem to reduce predicate logic results to corresponding ones of propositional logic. Thus, it is necessary, if covering this material, to do the propositional case first. The sections needed for the treatment of PROLOG are 1.8, 1.10 and II.11-13. The refinements of resolution considered in 1.9 are strictly optional. While linear resolution (II.14) is highly relevant to PROLOG, the completeness theorem is one of the most difficult in the text. We have therefore provided in III.1 an alternate approach to the corresponding results for Horn logic and PROLOG that requires only the basic definitions of linear resolution (I.14.1-3).
A diagram of the logical dependencies between sections of the text (except for Chapter VI) is given on the facing page. Unless Indicated otherwise by an arrow, the order of dependency runs right to left. Dotted lines (as from the propositional to predicate sections for classical logic) indicate relevance but not strict logical dependence. We should note that the very first section, I.1, simply collects definitions and facts about orderings and trees that are needed at various points in the text. This material can be covered at the beginning or inserted as needed. In particular, Konig's lemma, 1.1.4, is not needed until the treatment of complete systematic tableaux in 1.4. Similarly, the material on set-theoretic procedures in Chapter VI (new in this edition) can be covered at any point. Only one section (§6) assumes a familiarity with predicate logic and that is simply to list a formal version of the axioms. In this chapter, §§1-5 and §7 contain the basic set theory needed for this book and most undergraduate courses. The remaining sections, §§8-11, develop the theory of infinite (and even uncountable) ordinals, cardinals and transfinite recursion including some versions of the axiom of choice. This material should suffice as a background in set theory for most graduate courses in mathematics and computer science but is not used in the rest of this book.
At various other points in the text, certain paragraphs or even whole sections that are not needed for the later material are marked as optional by an asterisk (*). They are also printed in smaller type and with wider margins to set them off from the main line of development. In addition, there are three important possible exceptions to the order indicated above; these are of particular relevance for those courses not including very much about PROLOG. ..
The first exception also needs a warning. Our basic approach to logic does not include a specialized equality predicate. Although no longer the common approach in texts on mathematical logic, this is the right way to develop the subject to do resolution theorem proving, Logic Programming and PROLOG. We have thus relegated to III.5 the analysis of equality, either as a special predicate with the privileged semantics of true equality and the corresponding logical axiom schemes, or as an ordinary one with the appropriate equality axioms added on to each system under consideration. It is, however, quite possible to cover the relevant material in III.5 up to III.5.3 and the proofs of the soundness and completeness theorems for equality interpretations described there immediately after II.7.
The second exception concerns 'the proof of Church's theorem on the undecidability of validity for predicate logic. In III.8 we present a proof designed to apply even to the fragment of predicate logic represented in PROLOG. In Exercise 3 of III.5, however, we indicate how the presentation can easily be modified to make no mention of PROLOG notation or procedures and so give a proof of Church's theorem which is accessible after II.7.
Finally, the introduction to nonmonotonic logic given in III.7 up to III.7.6 can also be read independently of the material on Logic Programming and PROLOG. The rest of III.7 consists of an analysis of the stable models of Logic Programming with negation in terms of nonmonotonic logic. Other, more self-contained, applications to graphs and partial orders are given in Exercises 8-9 of III.7.
We should point out that there is a considerable overlap in the basic material for the development of modal and intuitionistic logic in Chapters IV and V. Indeed, a single unified development is possible albeit at some expense to the ease of intelligibility. We have instead written these chapters so that either may be read independently of the other. For the readers who wish to delve into both topics, we supply a comparative guide to basic notions of classical, modal and intuitionistic logic in V.6. We try there to point out the similarities and differences between these logics.
We have included a variety of problems at the end of almost every section of the text including a fair number of programming problems in PROLOO that can be assigned either for theoretical analysis or actual implementation. In particular, there are series of problems based on a database consisting of the genealogical lists in the first few chapters of Chronicles. It is reproduced in Appendix B. (An electronic version is available. Send an email request to shore@math.cornell.edu.) We have included these problems to serve as paradigms for use with a similar database or to be appropriately modified to fit other situations. This is not, however, a text on PROLOG programming. When teaching this material, we always supplement it with one of the standard texts on PROLOG programming listed in the suggestions for further reading at the end of Chapter III. Nothing in the text is tied to a particular version of the PROLOG language; we use only standard syntax and discuss typical implementations. We have ourselves used various implementations and platforms. The printouts of program runs are from ARITY PROLOG running on a PC.
When we (infrequently) cite results from the current literature, we attribute them as usual. However, as this is a basic textbook, we have made no attempt to attribute the standard results of the subject to their discoverers, other than when at times we name theorems according to common usage. We have, however, supplied a brief history of logic in an appendix that should give the student a feel for the development of the subject. In addition, suggestions for further reading that might be useful for either students or teachers using this text are given at the end of each chapter. Finally, a fairly extensive bibliography of related material, arranged by subject, is given at the end of the book.
Portions of this book appeared in various formats over many years. Very early versions of the material on classical logic and set theory appeared in lecture notes by Nerode which were distributed for courses at Cornell years ago. Part of this material was also independently reworked by George Metakides and appeared as lecture notes in English with Nerode and in Greek as his lectures at the University of Patras. Nerode [1990, 4.2] and [1991, 4.4] contain preliminary versions of our treatment of intuitionistic and modal logic based on the tableau method which were presented in lectures at Montecatini Terme and Marktoberdorf in 1988 and 1989, respectively. Our approach to resolution was also influenced by courses on program verification given by Richard Platek at Cornell. More current versions of the material have been read and used over the past years by a number of teachers in both mathematics and computer science departments and we have benefited considerably from their comments and suggestions. We should mention Uri Abraham (Mathematics, Ben Gurion University, Israel), John Crossley (Mathematics and Computer Science, Monash University, Australia), Ward Henson (Mathematics, University of Illinois, Urbana), Nils Klarlund (Computer Science, University of Aarhus, Denmark), Dexter Kozen (Computer Science, Cotnell) ,George Metakides (University of Patras, Greece and Information Technologies Research, EEC) and Jacob Plotkin (Mathematics, Michigan State University). Perry Smith (Math. Reviews) suggested Theorem 1.4.11 of this edition and its proof. Bakhadyr Khussainov pointed out an error in the previous edition in the proof of Theorem V.2.20. Warren Ooldfarb (Philosophy, Harvard) helped us avoid a number of pitfalls in the historical appendix. Particularly extensive (and highly beneficial)comments were received from Wiktor Marek (Computer Science, University of Kentucky), George Odifreddi (Computer Science, University of Turin, Italy) and Robert Soare (Mathematics and Computer Science, University of Chicago) who used several versions of the text in their courses. We also owe a debt to our graduate students who have served as assistants for our logic courses over the past few years and have made many corrections and suggestions: Jennifer Davoren, Steven Kautz, James Lipton, Sherry Marcus and Duminda Wijesekera.
We gratefully acknowledge the financial support over the past few years of the NSF under grants DMS-g601048, DMS-8902797, DMS-9204308, DMS-9503503; the ARO under grants DAAG29-85-C-O018 and DAAL03-91-C-0027 through ACSyAM at the Mathematical Sciences Institute of Cornell University; and IBM for an equipment grant through Project Ezra at Cornell University. We would also like to thank Arletta Havlik and Graeme Bailey for their help with the TEXing of the original version of the text for the previous edition as well as Geraldine Brady, Jennifer Davoren, Nathaniel Miller, Robert Miinikel, George Odifreddi and David Solomon for their help in proofreading.
Finally, in appreciation of their continuing support, we dedicate this book to our wives, Sally and Naomi. ...
Cornell University Anll Nerode
Ithaca, NY Richard A. Shore
June 1996
