Intellectics and Computational Logic APPLIED LOGIC SERIES VOLUME 19 Managing Editor Dov M. Gabbay, Department of Computer Science, King's College, London, U.K. Co-Editor John Barwise, Department of Philosophy, Indiana University, Bloomington, IN, U.S.A. Editorial Assistant Jane Spurr, Department of 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 sub jects 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 demon strates the underlying unity and applicability of logic. The titles published in this series are listed at the end of this volume. Intellectics and Computational Logic Papers in Honor of Wolfgang Bibel edited by STEFFEN HOLLDOBLER Dresden University of Technology, Germany 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-5438-8 ISBN 978-94-015-9383-0 (eBook) DOI 10.1007/978-94-015-9383-0 Printed on acid-free paper AlI Rights Reserved © 2000 Springer Science+Business Media Dordrecht OrigfnaIly published by Kluwer Academic Publishers in 2000 Softcover reprint ofthe hardcover lst edition 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 permis sion from the copyright owner WOLFGANG BffiEL TABLE OF CONTENTS STEFFEN HOLLDOBLER I Preface ix CHRISTOPH KREITZ I Prologue 1 PETER BAUMGARTNER, NORBERT EISINGER AND ULRICH 3 FURBACH I A Confluent Connection Calculus GERHARD BREWKA AND THOMAS BITER I Prioritizing Default 27 Logic STEFAN BRUNING AND TORSTEN SCHAUB I A Connection 47 Calculus for Handling Incomplete Information RICARDO CAFERRA AND NICOLAS PELTIER I The Connection 67 Method, Constraints and Model Building ROBERT DEMOLOMBE AND LUIS FARINAS DEL CERRO I Towards 85 a Logical Characterisation of Sentences of the Kind "Sentence p is About Object c" ELMAR EDER I The Cut Rule in Theorem Proving 101 UWE EGLY AND HANS TOMPITS I Some Strengths ofNonmonotonic 125 Reasoning JUTTA EUSTERBROCK I Composing Re-usable Synthesis Methods 143 through Graph-based Viewpoints BERTRAM FRONHOFER I Proof Structures and Matrix Graphs 159 CRISTOPH HERRMANN I AI and Cognitive Science: Feedback Leads to 175 a New Neural Concept CHRISTOPH KREITZ, JENS OTTEN, STEPHAN SCHMITT AND 189 BRIGITTE PIENTKA I Matrix-based Constructive Theorem Proving STEFFEN HOLLDOBLER AND HANS-PETER STORR I Complex 207 Plans in the Fluent Calculus GERHARD LAKEMEYER AND HECTOR J. LEVESQUE I Querying 225 AOL Knowledge Bases vii viii TABLE OF CONTENTS REINHOLD LETZ I Properties and Relations of Tableau and Connection 245 Calculi ERICA MELIS AND JORG H. SIEKMANN I Concepts in Proof Planning 263 J. A. ROBINSON I Proof= Guarantee+ Explanation 277 JOHANN SCHUMANN I Automated Theorem Proving in High-Quality 295 Software Design ANTJE STROHMAIER I A Complete Neural Network Algorithm for 313 HORN-SAT MICHAEL THIELSCHER I Nondeterministic Actions in the Fluent 327 Calculus: Disjunctive State Update Axioms CHRISTIAN WAGNER I The Illusion of Knowledge 347 CHRISTOPH WALTHER I Criteria for Termination 361 CHRISTOPH KREITZ I Epilogue 387 STEFFEN HOLLDOBLER PREFACE Intellectics is the field of science, where, on the one hand, an understanding of the functions, structure and operations of the human intellect is attempted and, on the other hand, artificial systems are tested to see to what extent they can substitute or complement such functions. The name "intellectics" was introduced in the early 1980s by Wolfgang Bibel as a linguistically correct name for the united fields of artificial intelligence and cognitive science. The field of intellectics can be divided into the subareas cognitive modeling, natural communication, robotics, machines and, at the very heart of it, knowledge based systems. The core of any intellectics system itself consists of a knowledge base together with an inference component. It is - and always was - this core which is the focus point of the research carried out by Wolfgang Bibel. Moreover, he is - and always was - a strong advocate for a formal basis of this core within a computational logic. Based on a solid education in physics, mathematics and, in particular, in mathemat icallogic, Wolfgang Bibel was among the few scientist who recognized the chances and potentials of artificial intelligence and cognitive science in the late 1960s. From this time on he devoted his energy to establish this field of science in Germany and Europe. Although he sometimes faced considerable difficulties, his efforts were ex tremely successful. Looking at the most influential events in the history of intellectics in Germany and Europe one almost always discovers the name of Wolfgang Bibel. The German Workshops on Artificial Intelligence, the German Spring Schools on Ar tificial Intelligence, the European Coordination Committee for Artificial Intelligence and the integration of our colleagues working in Eastern Europe are just a few of the activities that were co-founded and strongly supported by Wolfgang Bibel. Just a few months ago the German research focus programme on deduction, which was running since 1992 and was headed by Wolfgang Bibel, came to a very successful end. Today Germany is among the leading nations in this area. Wolfgang Bibel's own research was always focussed on deduction and computa tional logic. He is convinced that the knowledge needed to solve problems should be represented in a logic language and that calculi equipped with intelligent strategies are adequate mechanisms for solving these problems. In more than one hundred and fifty ix X STEFFEN HOLLDOBLER publications and more than one hundred scientific talks Wolfgang Bibel has argued for his ideas. Under his guidance several automated theorems provers were developed, which demonstrated the strength and power of "his" connection method in interna tional competitions. At the same time he was always interested in the applications of deduction and, in particular, he made considerable contributions to the areas of automated programming, program synthesis, logic programming, deductive planning and knowledge based systems. Wolfgang Bibel has received numerous awards, among which the following ones are the most prestigious: In 1990 he has been awarded the title of an "AAAI Fellow" by the American Association for Artificial Intelligence (AAAI) "in Recognition of Significant Contributions to the Field of Artificial Intelligence". In 1996 he has received the German Research Excellence Award for Artificial Intelligence from the Association of German AI Institutions. In 1999 he has received the Donald E. Walker Distinguished Service Award for his outstanding contributions and service to the international AI community. This book is a collection of papers by distinguished researchers, colleagues and former students of Wolfgang Bibel, who at one time have worked together with him. The papers were collected on the occasion of Wolfgang Bibel's sixtieth birthday. They were all reviewed by second readers. In the papers technical problems related to intel lectics and computational logic are discussed. The range of subjects presented includes automated deduction, logic programming, the logic based approach to intellectics, rea soning about actions and causality, knowledge representation and reasoning as well as applications thereof. Each contribution contains new, unpublished and reviewed results. The collection provides a state of the art account of the current capabilities and limitations of a computational logic approach to intellectics. In addition, Christoph Kreitz has added a prolog and an epilog. Both were written while Christoph Kreitz was working in Wolfgang Bibel's group in Darmstadt on the occasion of a christmas party. This shall demonstrate that working with Wolfgang Bibel was not just challenging and inspiring but also fun. ACKNOWLEDGMENTS I am grateful to the second readers who carefully read the manuscripts and provided valuable additional information: Susanne Biundo Gerhard Brewka Hans-Jiirgen Biirckert Ricardo Caferra Christian Eckes Norbert Eisinger UweEgly Bertram Fronhofer Ulrich Furbach Christoph Kreitz Reinhold Letz David McAllester Hans Jiirgen Ohlbach Horst Reichel Enno Sandner Torsten Schaub Josef Schneeberger Hans-Peter Storr Michael Thielscher In fact, Norbert Eisinger contributed that much to the paper that the authors decided to make him a co-author. PREFACE xi Maria Tiedemann helped a lot to come up with a complete list of researchers who had worked together with Wolfgang Bibel. Hans-Peter Storr produced the Latex style as well as the final layout. Maja von Wedelstedt was involved in many administrative tasks related to this book project. I would like to express many thanks to all of them. Steffen Holldobler