文档介绍：Otmane Ait Mohamed César Muñoz
Sofiène Tahar (Eds.)
Theorem Proving
in Higher Order Logics
21st International Conference, TPHOLs 2008
Montreal, Canada, August 18-21, 2008
Proceedings
13
Volume Editors
Otmane Ait Mohamed
Sofiène Tahar
Concordia University
Department of Electrical puter Engineering
1455 de Maisonneuve Blvd. W.
Montreal, Quebec, Canada H3G 1M8
E-mail: {ait,tahar}***@
César Muñoz
National Institute of Aerospace
100 Exploration Way Hampton, VA 23666, USA
E-mail: munoz@
Library of Congress Control Number: 2008931582
CR Subject Classification (1998): , , , ,
LNCS Sublibrary: SL 1 – puter Science and General Issues
ISSN 0302-9743
ISBN-10 3-540-71065-5 Springer Berlin Heidelberg New York
ISBN-13 978-3-540-71065-3 Springer Berlin Heidelberg New York
This work is subject to copyright. All rights are reserved, whether the whole or part of the material is
concerned, specifically the rights of translation, reprinting, re-use of illustrations, recitation, broadcasting,
reproduction on microfilms or in any other way, and storage in data banks. Duplication of this publication
or parts thereof is permitted only under the provisions of the German Copyright Law of September 9, 1965,
in its current version, and permission for use must always be obtained from Springer. Violations are liable
to prosecution under the German Copyright Law.
Springer is a part of Springer Science+Business Media
© Springer-Verlag Berlin Heidelberg 2008
Printed in Germany
Typesetting: Camera-ready by author, data conversion by Scientific Publishing Services, Chennai, India
Printed on acid-free paper SPIN: 12446179 06/3180 543210
Preface
This volume constitutes the proceedings of the 21st International Conference
on Theorem Proving in Higher Order Logics (TPHOLs 2008), which was held
during August 18–21, 2008 in Montreal, Canada. TPHOLs covers all aspects
of theorem proving in higher order logics as well as related topi