Mathematical Logic for Computer Science

answer yes if A ∈ U and the answer no if A ∈ U . If U is the set of satisfiable formulas, a decision procedure for U is called a decision procedure for satisfiability, and similarly for validity. By Theorem 2.39, a decision procedure for satisfiability can be used as a decision procedure for validity. To decide if A is valid, apply the ...
6MB Sizes 214 Downloads 393 Views
Mathematical Logic for Computer Science

Mordechai Ben-Ari

Mathematical Logic for Computer Science Third Edition

Prof. Mordechai (Moti) Ben-Ari Department of Science Teaching Weizmann Institute of Science Rehovot, Israel

ISBN 978-1-4471-4128-0 ISBN 978-1-4471-4129-7 (eBook) DOI 10.1007/978-1-4471-4129-7 Springer London Heidelberg New York Dordrecht Library of Congress Control Number: 2012941863 1st edition: © Prentice Hall International Ltd. 1993 © Springer-Verlag London 2009, 2012 This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or information storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now known or hereafter developed. Exempted from this legal reservation are brief excerpts in connection with reviews or scholarly analysis or material supplied specifically for the purpose of being entered and executed on a computer system, for exclusive use by the purchaser of the work. Duplication of this publication or parts thereof is permitted only under the provisions of the Copyright Law of the Publisher’s location, in its current version, and permission for use must always be obtained from Springer. Permissions for use may be obtained through RightsLink at the Copyright Clearance Center. Violations are liable to prosecution under the respective Copyright Law. The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. While the advice and information in this book are believed to be true and accurate at the date of publication, neither the authors nor the editors nor the publisher can accept any legal responsibility for any errors or omissions that may be made. The publisher makes no warranty, express or implied, with respect to the material contained herein. Printed on acid-free paper Springer is part of Springer Science+Business Media (www.springer.com)

For Anita

Preface

Students of science and engineering are required to study mathematics during their first years at a university. Traditionally, they concentrate on calculus, linear algebra and differential equations, but in computer science and engineering, logic, combinatorics and discrete mathematics are more appropriate. Logic is particularly important because it is the mathematical basis of software: it is used to formalize the semantics of programming languages and the specification of programs, and to verify the correctness of programs. Mathematical Logic for Computer Science is a mathematics textbook, just as a first-year calculus text is a mathematics textbook. A scientist or engineer needs more than just a facility for manipulating formulas and a firm foundation in mathematics is an excellent defense against technological obsolescence. Tempering this requirement for mathematical competence is the realization that applications use only a fraction of the theoretical results. Just as the theory of calculus can be taught to students of engineering without the full generality of measure theory, students of computer science need not be taught the full generality of uncountable structures. Fortunately (as shown by Raymond M. Smullyan), tableaux provide an elegant way to teach mathematical logic that is both theoretically sound and yet sufficiently elementary for the undergraduate.

Audience The book is intended for undergraduate computer science students. No specific mathematical knowledge is assumed aside from informal set theory which is summarized in an appendix, but elementary knowledge of concepts from computer science (graphs, languages,