Handbook.of.Practical.Logic.and.Automated.Reasoning,.Harrison,.CUP,.2009.pdf

This page intentionally left blank
HANDBOOK OF PRACTICAL LOGIC
AND AUTOMATED REASONING
John Harrison
The plexity puter systems has meant that automated rea-
soning, . the use puters to perform logical inference, has e
a ponent of program construction and of programming language
design. This book meets the demand for a self-contained and broad-based
account of the concepts, the machinery and the use of automated reasoning.
The mathematical logic foundations are described in conjunction with their
practical application, all with the minimum of prerequisites.
The approach is constructive, concrete and algorithmic: a key feature is
that methods are described with reference to actual implementations (for
which code is supplied) that readers can use, modify and experiment with.
This book is ideally suited for those seeking a one-stop source for the gen-
eral area of automated reasoning. It can be used as a reference, or as a place
to learn the fundamentals, either in conjunction with advanced courses or
for self study.
John Harrison is a Principal Engineer at Intel Corporation in Portland,
Oregon. He specialises in formal verification, automated theorem proving,
floating-point arithmetic and mathematical algorithms.
HANDBOOK OF PRACTICAL LOGIC
AND AUTOMATED REASONING
JOHN HARRISON
CAMBRIDGE UNIVERSITY PRESS
Cambridge, New York, Melbourne, Madrid, Cape Town, Singapore, São Paulo
Cambridge University Press
The Edinburgh Building, Cambridge CB2 8RU, UK
Published in the United States of America by Cambridge University Press, New York
Information on this title: 0521899574
© J. Harrison 2009
This publication is in copyright. Subject to statutory exception and to the
provision of relevant collective licensing agreements, no reproduction of any part
may take place without the written permission of Cambridge University Press.
First published in print format 2009
ISBN-13 978-0-511-50865-3 eBook (NetLibrary)
ISBN-13 978-0-521-89957-4 har