The Seventeen Provers of the World Foreword by Dana S. Scott
Commemorating the 50th anniversary of the first time a mathematical theorem was proven by a computer system, Freek Wiedijk initiated the present book in 2004 by inviting formalizations of a proof of the irrationality of the square root of two from scienti
- PDF / 1,248,402 Bytes
- 172 Pages / 430 x 660 pts Page_size
- 72 Downloads / 167 Views
Subseries of Lecture Notes in Computer Science
3600
Freek Wiedijk (Ed.)
The Seventeen Provers of the World Foreword by Dana S. Scott
13
Series Editors Jaime G. Carbonell, Carnegie Mellon University, Pittsburgh, PA, USA Jörg Siekmann, University of Saarland, Saarbrücken, Germany Volume Editor Freek Wiedijk Radboud University Institute for Computing and Information Sciences Postbus 9010, 6500 GL Nijmegen, The Netherlands E-mail: [email protected]
Library of Congress Control Number: 2005939043
CR Subject Classification (1998): I.2.3, I.2, F.4.1, F.4, D.2 LNCS Sublibrary: SL 7 – Artificial Intelligence ISSN ISBN-10 ISBN-13
0302-9743 3-540-30704-4 Springer Berlin Heidelberg New York 978-3-540-30704-4 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 springeronline.com © Springer-Verlag Berlin Heidelberg 2006 Printed in Germany Typesetting: Camera-ready by author, data conversion by Boller Mediendesign Printed on acid-free paper SPIN: 11542384 06/3142 543210
Editorial
This volume starts a new subline of Lecture Notes in Artificial Intelligence, called AI-SYSTEMS focusing on the most important systems and prototypical developments in artificial intelligence. We have chosen an initiative of the year 2004 as the starting date to commemorate the 50th anniversary of the first time a mathematical theorem was proven by a computer system: Martin Davis’ implementation of the Presburger Fragment of first-order logic proved the mind-stretching result that the sum of two even numbers is again even. While the first volumes in this category will present – for historical reasons – today’s internationally most relevant systems from the field of automated reasoning, we shall soon solicit detailed presentations of individual systems as well as systems from the other major subareas of AI.
October 2005
J¨ org Siekmann Alfred Hofmann
Foreword
Our compiler, Freek Wiedijk, whom everyone interested in machine-aided deduction will thank for this thought-provoking collection, set his correspondents the problem of proving the irrationality of the square root of 2. That is a nice, straight-forward question. Let’s think about it geometrically – and intuitively. The original question involved comparing the side with the diagonal of a square. This reduces to looking at an isosceles right triangle. For such a triangle, the proof of the Pythagorean Theorem is obvious. As we can see from the figure, the squares on the legs are made up
Data Loading...
