logo资料库

A Logical Approach to Discrete Math.pdf

第1页 / 共520页
第2页 / 共520页
第3页 / 共520页
第4页 / 共520页
第5页 / 共520页
第6页 / 共520页
第7页 / 共520页
第8页 / 共520页
资料共520页,剩余部分请下载后查看
TEXS AND MONOGRAPHS IN COMPUTER SCIENCE A LOGICAL APPROACH TO DISCR David Gr.e Fred B. Schneider MATH I -TL - I neorem: (Vx I P * Q) g- S : * '- {x P} C {x [ Q} q Proof: {x I P} C {x [ Q} (Def. of Subset C,,, with v not occurring free in P or Q) I v {x P}:v E{x I Q}) ( (V |x I RI -= R A: iv:wice) (Vv I P[x - v] : Q[* := v]) (Trading; Dummy renaming (YX I P[x - v][v:Ax XI Q[x - vv :] = x]) | (R[x:V][v:XI = R if v does not occur free in 'R twce (VxI: P =iQ Q) f < . . iE iti; . g . / . Ps @1 L:s .. 4 : gAlwz SprinWrQrlag X ME y,
Table of Precedences [x := e] (textual substitution) . (function application) unary prefix operators: + ** * / ± mod gcd + - u n x o - #I - > C D = < > G C C D 2 V A (highest precedence) - # P (conjunctional, see page 29) - (lowest precedence) (a) (b) (c) (d) (e) (f) (g) (h) (i) (j) (k) (1) (m) All nonassociative binary infix operators associate to the left, except **, a , and ', which associate to the right. The operators on lines (j), (1), and (in) may have a slash / them to denote negation -e.g. through b # c is an abbreviation for -(b =- c) . Greek letters and their Transliterations Name Alpha Beta Gamma Delta Epsilon Zeta Eta Theta a fi y 6 e Sign It. a b g d e z e th 7i V Name Iota b Kappa n Lambda A Mu Nu Xi Omicron Pi Sign Tr. i k I A m n v x o p o 7r Name Rho Sigma Tau Upsilon Phi Chi Psi Omega Types Used in this Text Sign TPr. r s t p a r- v 0 X 4b w y, u ph ch ps o z N Z+ 2- Q P integer nat positive negative rational reals positive reals R+ bool sets bags sequences integers: . .. ,-3,-2,-1,0,1,2,3.... natural numbers: 0, 1, 2 .. positive integers: 1, 2, 3 .... negative integers: 1, 2, 3,... rationals i/i for ii real numbers positive real numbers booleans: true, false B set of elements of type t set (t) bag(t) bag of elements of type t seq(t) sequence of elements of type t integers, j $4 0
Texts and Monographs in Computer Science Editors David Gries Fred B. Schneider Advisory Board F.L. Bauer S.D. Brookes C.E. Leiserson M. Sipser
Texts and Monographs in Computer Science Suad Alagic Object-Oriented Database Programming 1989. XV, 320 pages, 84 illus. Suad Alagic Relational Database Technology 1986. Xl, 259 pages, 114 illus. Suad Alagic and Michael A. Arbib The Design of Well-Structured and Correct Programs 1978. X, 292 pages, 68 illus. S. Thomas Alexander Adaptive Signal Processing: Theory and Applications 1986. IX, 179 pages, 42 illus. Krzysztof R. Apt and Ernst-Rudiger Olderog Verification of Sequential and Concurrent Programs 1991. XVI, 441 pages Michael A. Arbib, A.J. Kfoury, and Robert N. Moll A Basis for Theoretical Computer Science 1981. VIII, 220 pages, 49 illus. Friedrich L. Bauer and Hans Wossner Algorithmic Language and Program Development 1982. XVI, 497 pages, 109 illus. W. Bischofberger and G. Pomberger Prototyping-Orlented Software Development: Concepts and Tools 1992. XI, 215 pages, 89 illus. Ronald V. Book and Friedrich Otto String-Rewriting Systems 1993. Vii, 200 pages Kaare Christian A Guide to Modula-2 1986. XIX, 436 pages, 46 illus. Edsger W. Dijkstra Selected Writings on Computing: A Personal Perspective 1982. XVII, 362 pages, 13 illus. (continued after ind4
A Logical Approach to Discrete Math David Gries Fred B. Schneider With 25 Illustrations I Springer-Verlag New York Berlin Heidelberg London Paris Tokyo Hong Kong Barcelona Budapest
David Gries Department of Computer Science Cornell University Upson Hall Ithaca, NY 14853-7501 USA Fred B. Schneider Department of Computer Science Cornell University Upson Hall Ithaca, NY 14853-7501 USA Library of Congress Cataloging-in-Publication Data Gries, David. 11st ed] A logical approach to discrete math / David Gries and Fred B. cm. - (Texts and monographs in computer science) Includes bibliographical references and index. ISBN 0-387-94115-0 1. Mathematics. I. Schneider, Fred B. II. Title. Schneider. p. QA39.2.G7473 1994 51 0-dc2O Ill. Series. 93-27848 Printed on acid-free paper. © 1993 Springer-Verlag New York, Inc. All rights reserved. This work may not be translated or copied in whole or in part with( the written permission of the publisher (Springer-Verlag New York, Inc., 175 Fifth Aveni New York, NY 10010, USA), except for brief excerpts in connection with reviews or sc& arly analysis. Use in connection with any form of information storage and retrieval, ell tronic adaptation, computer software, or by similar or dissimilar methodology now kno, or hereafter developed is forbidden. The use of general descriptive names, trade names, trademarks, etc., in this publication even if the former are not especially identified, is not to be taken as a sign that such naml as understood by the Trade Marks and Merchandise Marks Act, may accordingly be us freely by anyone. Production managed by Hal Henglein; manufacturing supervised by Jacqui Ashri. Photocomposed copy produced from the authors' LaTeX files. Printed and bound by Braun-Brumfield, Ann Arbor, Ml. Printed in the United States of America. 987654321 ISBN 0-387-94115-0 Springer-Verlag New York Berlin Heidelberg ISBN 3-540-94115-0 Springer-Verlag Berlin Heidelberg New York
To the women in our lives, Elaine and Mimi
Preface This text attempts to change the way we teach logic to beginning students. Instead of teaching logic as a subject in isolation, we regard it as a basic tool and show how to use it. We strive to give students a skill in the propo- sitional and predicate calculi and then to exercise that skill thoroughly in applications that arise in computer science and discrete mathematics. We are not logicians, but programming methodologists, and this text reflects that perspective. We are among the first generation of scientists who are more interested in using logic than in studying it. With this text, we hope to empower further generations of computer scientists and math- ematicians to become serious users of logic. Logic is the glue Logic is the glue that binds together methods of reasoning, in all domains. The traditional proof methods -for example, proof by assumption, con- tradiction, mutual implication, and induction- have their basis in formal logic. Thus, whether proofs are to be presented formally or informally, a study of logic can provide understanding. But we want to impart far more than the anatomy of the glue proof theory and model theory. We want to impart a skill in its use. For this rea- son, we emphasize syntactic manipulation of formulas as a powerful tool for discovering and certifying truths. Of course, syntactic manipulation cannot completely replace thinking about meaning. However, the discomfort with and reluctance to do syntactic manipulation that accompanies unfamiliar- ity with the process unnecessarily forces all reasoning to be in terms of meaning. Our goal is to balance the tendency to reason semantically with the ability to perform syntactic reasoning. Students thereby acquire under- standing of when syntactic reasoning is more suitable, as well as confidence in applying it. When we teach the propositional and predicate calculi, students are put in a syntactic straightjacket. Proofs must be written rigorously. This is an advantage, not a disadvantage, because students learn what it means for a proof to be rigorous and that rigor is easily achieved. We also describe prin- ciples and strategies for developing proofs and go over several proofs for the same theorem, discussing their advantages and disadvantages. Gradually,
分享到:
收藏