Proofs and Algorithms An Introduction to Logic and Computability

Proofs and Algorithms: An Introduction to Logic and ComputabilityLogic is a branch of philosophy, mathematics and computer science. It studies the required methods to determine whether a statement is true, such as reasoning and computation.

Proofs and Al

  • PDF / 1,287,967 Bytes
  • 160 Pages / 439.37 x 666.142 pts Page_size
  • 95 Downloads / 311 Views

DOWNLOAD

REPORT


Undergraduate Topics in Computer Science (UTiCS) delivers high-quality instructional content for undergraduates studying in all areas of computing and information science. From core foundational and theoretical material to final-year topics and applications, UTiCS books take a fresh, concise, and modern approach and are ideal for self-study or for a one- or two-semester course. The texts are all authored by established experts in their fields, reviewed by an international advisory board, and contain numerous examples and problems. Many include fully worked solutions.

For further volumes: www.springer.com/series/7592

Gilles Dowek

Proofs and Algorithms An Introduction to Logic and Computability

Gilles Dowek École Polytechnique Palaiseau France [email protected]

Series editor Ian Mackie Advisory board Samson Abramsky, University of Oxford, Oxford, UK Chris Hankin, Imperial College London, London, UK Dexter Kozen, Cornell University, Ithaca, USA Andrew Pitts, University of Cambridge, Cambridge, UK Hanne Riis Nielson, Technical University of Denmark, Lungby, Denmark Steven Skiena, Stony Brook University, Stony Brooks, USA Iain Stewart, University of Durham, Durham, UK

Based on course notes by Gilles Dowek, published simultaneously in French by École Polytechnique with the following title: “Les démonstrations et les algorithmes”. The translator of the work is Maribel Fernandez. ISSN 1863-7310 ISBN 978-0-85729-120-2 e-ISBN 978-0-85729-121-9 DOI 10.1007/978-0-85729-121-9 Springer London Dordrecht Heidelberg New York British Library Cataloguing in Publication Data A catalogue record for this book is available from the British Library © Springer-Verlag London Limited 2011 Apart from any fair dealing for the purposes of research or private study, or criticism or review, as permitted under the Copyright, Designs and Patents Act 1988, this publication may only be reproduced, stored or transmitted, in any form or by any means, with the prior permission in writing of the publishers, or in the case of reprographic reproduction in accordance with the terms of licenses issued by the Copyright Licensing Agency. Enquiries concerning reproduction outside those terms should be sent to the publishers. The use of registered names, trademarks, etc., in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant laws and regulations and therefore free for general use. The publisher makes no representation, express or implied, with regard to the accuracy of the information contained in this book and cannot accept any legal responsibility or liability for any errors or omissions that may be made. Printed on acid-free paper Springer is part of Springer Science+Business Media (www.springer.com)

Acknowledgements

The author would like to thank René Cori, René David, Maribel Fernández, JeanBaptiste Joinet, Claude Kirchner, Jean-Louis Krivine, Daniel Lascar, Stéphane Lengrand, Michel Parigot, Laurence Rideau and Paul Rozière.

v

Contents

Part I

Proofs

1

Pred