Wolfgang Bibel Automated Theorem Proving Wolfgang Bibel Automated Theorem Proving Friedr. Vieweg & Sohn Braunschweig IWiesbaden CIP-Kurztitelaufnahme der Deutschen Bibliothek Bibel, Wolfgang: Automated theorem proving I Wolfgang Bibel. - Braunschweig; Wiesbaden: Vieweg, 1982. 1982 All rights reserved © Friedr. Vieweg & Sohn Verlagsgesellschaft mbH, Braunschweig 1982 No part of this publication may be reproduced, stored in a retrieval system or transmitted in any form or by any means, electronic, mechanical, photocopying, recording or otherwise, with out prior permission of the copyright holder. ISBN-13: 978-3-528-08520-9 e-ISBN-13: 978-3-322-90100-2 DOl: 10.1007/978-3-322-90100-2 Preface Among the dreams of mankind is the one dealing with the mecha nization of human thought. As the world today has become so complex that humans apparently fail to manage it properly with their intellectual gifts, the realization of this dream might be regarded even as something like a necessity. On the other hand, the incredible advances in computer technology let it appear as a real possibility. Of course, it is not easy to say what sort of thing human thinking actually is, a theme which over the centuries occupied many thinkers, mainly philosophers. From a critical point of view most of their theories were of a speculative nature since their only way of testing was by Gedanken-experi ments. It is the computer which has opened here a wide range of new possibilities since with this tool we now can model real experiments and thus test such theories like physicists do in their field. About a quarter of a century ago, scientific activi ties of that sort were started under the label of artificial intelligence Today these activities establish a wide and prosperous field which the author, in lack of any better name, prefers to call intellectics. Without any doubt, the com puter programs developed in this field have tought us much about the nature of human thinking. One of its prominent features is the ability for logi cal reasoning which had been studied extensively by the logi cians of many centuries. In particular, their contributions within the last hundred years have prepared the grounds for the mechanization of this special feature. Although reasoning certainly is part of most intellectual activities, it naturally plays a particularly important role in mathematics. Not sur prisingly then, the first attempts towards automatic reasoning were made in mathematical applications focusing on generating VI proofs of mathematical theorems. For this historical reason, this subarea within intellectics is still identified as automated theorem proving although proving mathematical theorems is just one in a wide variety of applications. The purpose of this book is to prov ide a comprehens i ve development of the most advanced basic deductive tools present ly available in this area and to give an idea of their useful ness for many important applications. Because of the rapid expansion of this field, which in a wider sense also is termed automated deduction , it is certainly not possible any more to cover all its aspects in a single book. Hence our attention will focus on the classical tool of proof procedures for first order logic which in our opinion are to be regarded as basic for the whole field, at least for the time being. In the 1970' s much research in this area has concen trated on how to el iminate the enormous redundancy experienced in running computer systems which realized such proof proce dures. Much of it was based on resolution, but some was car ried out also with a rather different background. With our uni form treatment based on what we call the connection method we hope to have re-combined these various attempts into one single stream of research, which culminates in the description of what, accord ing to current technology, appear to be the fea tures of a most advanced proof procedure for first-order logic. Unfortunately, these features have become so complex that any author dealing with this topic faces a real problem of presentation. On the one hand, because of this complexity a rigorous treatment is of essential importance in order to avoid serious errors or misjudgements. On the other hand, many readers will be frightened by the resultant formalism, thus creating the need for plenty of illustrations and informal descriptions. We have made an attempt to serve both these needs by pairing the rigorous definitions, thorems and proofs with informal descriptions and discussions, illustrated with many examples. If this attempt has been successful then the book might actually serve for a wide spectrum of readers. On the one extreme, there would be those who just want to understand the ideas behind all the formalism and thus study the examples VII guided by the informal discussions without going much into the details of formal definitions, theorems and proofs. On the other extreme, well-trained logicians might easily skip much of the informal text. And in the middle there are those readers who are grateful for informal explanations but also acknowledge the necessity of preciseness for such a complex topic, and thus read both these approaches in parallel . The ability to read mathematical definitions, theorems and proofs together with some basic knowledge about elementary set theory and about algorithms are actually all the pre requisites needed for a full understanding of most parts of the book. However, some familiarity with mathematical logic and/or some previous training in abstract mathematical think ing will certainly be helpful for coping with the intrinsic complexity of some of the results. Although this book has not been explicitly designed as a textbook it may well be used in instructor-student settings. For such purposes a number of exercises of varied difficulties may be found at the end of each chapter 1 isted in the sequence of the presented topics. The selection of material for such a course should be easy with the following hints. Chapter I provides a short introduction into logic as the formal structure of natural reasoning. The basic connec tion method is then developed, first, in chapter II, on the level of propositional logic and second, in a strictly par allel treatment in chapter III, on the level of first-order logic. This, together with the first two sections in chapter IV, which introduce resolution and embed it into the connec tion method, is regarded as the basis for the field of auto mated theorem proving. The rest of chapter IV contains more specialized material on the connection method towards a most advanced proof system for first-order logic, which will be of partic ular interest for researchers specializing in this field. Readers with a more general interest might rather consider the material in chapter V, perhaps even at an earlier stage of their reading. It briefly introduces some of the possible applications and extensions of first-order theorem proving. VIII Each chapter is preceded by a more detailed overview of its contents for further orientation. Moreover, the many references to previous or later parts of the book within the text should ease to begin reading at any of its parts. For this purpose we use a familiar numbering scheme. For instance, (III.3.5) refers to the item labeled 3.5 in chapter III. By convention, the number of the chapter is deleted for any reference within the actual chapter, that is, within chapter tIl the previous reference is simply (3.5) rather than (III.3.5). The same applies to figures and tables which, how ever, are numbered independently. The abbreviations used are generally familiar and are listed in table below. Also with our denotations we have tried to follow common practice as listed in table 2 and 3. Both, the historical remarks at the end of each chap ter and the bibliography as a whole are by no means comprehen sive. Rather, they reflect both, the author's limited knowl edge of an exploding literature and their direct relevance to the topics we consider in this book. Finally, we hope that the reader acknowledges the author's difficulty in expressing the material in a non-native language. Munchen, Dezember 1981 w. Bibel ACKNOWLEDGEMENTS Man ist geneigt, die Vollendung eines solchen Buches als ein personlich wichtiges Teilziel zu interpretieren, das stellver tretend fur vieles andere im eigenen Leben steht. Deshalb sieht man sich bei solcher Gelegenheit auch zum Ruckblick auf die Einflusse veranlaJ3t, (He den Weg bis hierher mitbestimmt haben. lch mul3 gestehen, dal3 mir jede Auswahl unter solchen Einflussen und die damit verbundene Gewichtung zumindest an fechtbar, wenn nicht sogar willkurlich erscheint. Deshalb IX mochte ich nur feststellen, da~ ich dankbar an viele Menschen denke, die mich in Liebe, Freundschaft, manche auch in Ha~ oder Gegnerschaft auf meinem Weg gefordert haben. Die vorbildliche Gestaltung des Textes selbst verdan ken wir aIle dem auf3erordentlichen Geschick von Frl. H. Hohn, die mit unermudlichem Einsatz aIle Schwierigkeiten zu meistern verstand. Bei den zeichnungen und Sonderzeichen war zudem Frau A. Bussmann behilflich. Dr. K.-M. Hornig sowie Herrn A. Muller bin ich fur viele Korrekturen und Verbesserungsvorschlage dankbar. Ihnen verdanke ich auch manche Anregung aus der ge meinsamen projektarbeit. Oem Fachbereich Informatik der Hoch schule der Bundeswehr Munchen, insbesondere Herrn Prof. W. Hahn, bin ich fur die Erlaubnis zur Benutzung eines Textauto maten verpflichtet. Herrn Prof. K. Mehlhorn sei fur die an den Verlag gegebene Anregung eines solchen Buches gedankt. Meine Musikfreunde, jedoch besonders meine Frau und meine Kinder haben mir die mit der Niederschrift verbundenen Muhen ertraglicher gemacht, wodurch sie einen nicht unbe trachtlichen Anteil an der Fertigstellung haben • .l I.bbreviation Intended meaning ATP Automated Theorem Proving fol first-order logic w.r.t. with respect to iff if and only if A iff B iff C A iff Band B iff C D. Definition T. Theorem L. Lemma C. Corollary F. Formula q.e.d. quod erat demonstrandum (what had to be proved) o end of proof or definition Table 1. List of abbreviations x Kind of objects Standard Symbols propositional variables P, Q, R constant symbols a, b, c function symbols f, g, h terms s, t predicate symbols P, Q, R signum or arity n literals K, L, M object variables x, y, z formulas, matrices 0, E, F clauses c, d, e paths p, q connections u, v, w sets of connections U, V, W connection graphs G, H natural numbers m, n, I indices i, j, k sets of indices I, J occurrences, positions r substitutions p, (J truth values T Comment. All symbols may be decorated with indices etc. Table 2. Standardized denotations XI N'otation Meaning n \;' m, sum, product i~1 1 set of natural numbers with 0 EN 1N o empty set v,n union, intersection set difference X\.:JY union in the special case XnY o b, i~ union, intersection with Xi , xi A ~ Xl' = 0, Xl' 0 i= 1 i= 1 number of elements in set X, i.e. cardinality of X X x Y cartesian product of X and Y Xn, X*, X+ n-fold product, ~ Xi , MCD Xi 2X set of subsets in X n mod m n modulo m Table 3. Standard notations