Goal-Directed Proof Theory
Goal Directed Proof Theory presents a uniform and coherent methodology for automated deduction in non-classical logics, the relevance of which to computer science is now widely acknowledged. The methodology is based on goal-directed provability. It is a g
- PDF / 22,567,111 Bytes
- 273 Pages / 438.832 x 667.507 pts Page_size
- 51 Downloads / 225 Views
APPLIED LOGIC SERIES VOLUME 21
Managing Editor Dov M. Gabbay, Department o/Computer Science, King's College, London, U.K.
Co-Editor Jon Barwiset
Editorial Assistant Jane Spurr, Department 0/ Computer Science, King's College, London, u.K.
SCOPE OF THE SERIES Logic is applied in an increasingly wide variety of disciplines, from the traditional subjects of philosophy and mathematics to the more recent disciplines of cognitive science, computer science, artificial intelligence, and linguistics, leading to new vigor in this ancient subject. Kluwer, through its Applied Logic Series, seeks to provide a home for outstanding books and research monographs in applied logic, and in doing so demonstrates the underlying unity and applicability of logic.
The titles published in this series are listed at the end of this volume.
Goal-Directed Proof Theory by
DOV M . GABBAY King's College, London, United Kingdom
and
NICOLA OLIVETTI Universita di Torino, Torino, Italy
SPRINGER-SCIENCE+BUSINESS MEDIA, B.V.
A C.I.P. Catalogue record for this book is available from the Library of Congress.
ISBN 978-90-481-5526-2 ISBN 978-94-017-1713-7 (eBook) DOI 10.1007/978-94-017-1713-7
Printed on acid-free paper
AII Rights Reserved © 2000 Springer Science+Business Media Dordrecht Originally published by Kluwer Academic Publishers in 2000 No part of the material protected by this copyright notice may be reproduced or utilized in any form or by any means, electronic or mechanical, including photocopying, recording or by any information storage and retrieval system, without written permission from the copyright owner
FOREWORD
This book contains the beginnings of our research program into goal-directed deduction. The idea of presenting logics in a goal-directed way was conceived in 1984 when the first author was teaching logic at Imperial College, London. The aim was to formulate the entire classical logic in a goal-directed Prolog-like way see the book [Gabbay, 1981] and [Gabbay, 1998]. This formulation for both classical and intuitionistic logic was successful and gave rise to an early version of the Restart rule and N -Prolog, the first extension of Hom clause programming with hypothetical implication (1984-1985). Since that time, several authors and research groups have adopted the goal-directed methodology either as a favourite deduction system for some specific logic or as a favourite extension of Prolog. In this book we present goal-directed deduction as a methodology to be applied to major families of non-classical logics. From the point of view of automated deduction, what makes goal-directedness a desirable presentation is that it drastically reduces the non-determinism in proof search. Moreover, a goal-directed procedure is by definition capable of focusing on the relevant data for the proof of the goal, ignoring the rest. Even if this may seem a minor point in small theoremproving examples, it is a most important feature if non-classical logics are to be used to specify deductive databases or logic programs. Whenever the s
