Artificial Intelligence Editors: S. Amarel A. Biermann L. Bole P. Hayes A. Joshi D. Lenat D. W. Loveland (Managing Editor) A. Mackworth D. Nau R. Reiter E. Sandewall S. Shafer Y. Shoham J. Siekmann W. Wahlster v. W Marek M. Truszczynski Nonmonotonic Logic Context-Dependent Reasoning Foreword by Ray Reiter Springer-Verlag Berlin Heidelberg GmbH V. Wiktor Marek Miroslaw Truszczynski Department of Computer Science, University of Kentucky Lexington, KY 40506-0027, USA CR Subject Classification (1991): 1.2.0, 1.2.3-4, FA.O-1 With 14 Figures ISBN 978-3-662-02908-4 Library of Congress Cataloging-in-Publication Data Marek. V. Wiktor. 1943- . Nonmonotonic logic: context-dependent reasoning / V. Wiktor Marek, M. Truszczynski. p. cm. - (Artificial intelligence) (Berlin, Germany) ISBN 978-3-662-02908-4 ISBN 978-3-662-02906-0 (eBook) DOI 10.1007/978-3-662-02906-0 I. Artificial intelligence. 2. Reasoning. 3. Optoelectronics. I. Truszczynski, Miroslaw. II. Title. III. Series. Q335.M37 1993 006.3-dc20 93-31084 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, reuse 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-Verlag Berlin Heidelberg GmbH. Violations are liable for prosecution under the German Copyright Law. © Springer-Verlag Berlin Heidelberg 1993 Originally published by Springer -Verlag Berlin Heidelberg New York in 1993 Softcover reprint of the hardcover 1st edition 1993 The use of general descriptive names, registered names, trademarks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. Typesetting: Camera-ready by authors 45/3140 -5 4 3 2 I 0 -Printed on acid-free paper To Ela, Malgosia and Natalia W.M. To Lena, Ania and Na talka M.T. Foreword When I first participated in exploring theories of nonmonotonic reasoning in the late 1970s, I had no idea of the wealth of conceptual and mathematical results that would emerge from those halting first steps. This book by Wiktor Marek and Miroslaw Truszczynski is an elegant treatment of a large body of these results. It provides the first comprehensive treatment of two influen tial nonmonotonic logics - autoepistemic and default logic - and describes a number of surprising and deep unifying relationships between them. It also relates them to various modal logics studied in the philosophical logic litera ture, and provides a thorough treatment of their applications as foundations for logic programming semantics and for truth maintenance systems. It is particularly appropriate that Marek and Truszczynski should have authored this book, since so much of the research that went into these results is due to them. Both authors were trained in the Polish school of logic and they bring to their research and writing the logical insights and sophisticated mathematics that one would expect from such a background. I believe that this book is a splendid example of the intellectual maturity of the field of artificial intelligence, and that it will provide a model of scholarship for us all for many years to come. Ray Reiter Department of Computer Science University of Toronto Toronto, Canada M5S 1A4 and The Canadian Institute for Advanced Research Table of Contents 1 Introduction ......... 1 1.1 The subject of this book 1 1.2 What do we do in this book? 4 1.3 To whom do we address this book? 5 1.4 The contents of this book 6 1.5 Acknowledgments ..... 8 2 Rudiments of logic and set theory 9 2.1 Syntax of propositional logic 9 2.2 Semantics of propositional logic 11 2.3 Proof theory for propositional logic 17 2.4 Completeness and compactness of propositional logic 20 2.5 Relations, partial orderings 21 2.6 Elements of predicate logic 23 2.7 Well-orderings, ordinal numbers. 31 2.8 Monotone operators ....... 34 3 General default theories .......... 37 3.1 Monotone rules in propositional logic . 38 3.2 Default logic - motivation 46 3.3 Default logic - syntax. . . 50 X Table of Contents 3.4 Extensions for default theories 51 3.5 Two more characterizations of extensions 61 3.6 Properties of default theories 66 3.7 Extensions and well-orderings 71 3.8 Prioritized default theories. 82 3.9 Computing extensions . . . 84 3.10 Other structures associated with default theories 87 3.11 Partial extensions .... 94 3.12 Comments and remarks 101 4 Normal default theories . . . 105 4.1 Normal default theories 105 4.2 Properties of normal default theories 109 4.3 The Closed World Assumption 111 4.4 Comments and remarks . . . . 123 5 Representation theory for default logic 125 5.1 Representability of default theories 125 5.2 Semi-representability of default theories 132 5.3 A representation result for weak extensions 137 5.4 Comments and remarks .......... . 139 6 Logic programming and nonmonotonic reasoning 141 6.1 Logic programs - basic definitions 141 6.2 Horn programs . . . . . . . . . . . 147 6.3 Stable models of general logic programs 149 6.4 Supported models of logic programs .. 152 6.5 Logic programming with classical negation. 159 6.6 Clausal logic programming. . . . ..... . 170 6.7 Stratified and locally stratified logic programs 172 Table of Contents XI 6.8 Proof schemes and stable models 182 6.9 Comments and remarks 186 7 Modal logic . . . . . . . . . . . . . . . . . . . . . 189 7.1 Modal logics - syntax and basic properties 189 7.2 General Kripke semantics . . . . . 200 7.3 Kripke semantics for normal logics 210 7 A Index logics . . . . . . . 218 7.5 Comments and remarks 222 8 Stable theories ...... . . 223 8.1 Stable theories and their elementary properties 223 8.2 Characterizations of stable theories 228 8.3 Algorithms ...... . 238 804 Comments and remarks 247 9 Modal nonmonotonic logics . . . . . . . . . . . . 249 9.1 Context-dependent proofs in a modal logic . 250 9.2 S-expansions and their elementary properties 252 9.3 Minimal model semantics ........ . 259 904 Consistency with respect to introspection 271 9.5 Characterization of S-expansions 279 9.6 Comments and remarks ..... 287 10 Nonmonotonic logic of pure necessitation and autoepistemic logics 289 10.1 Nonmonotonic logic N . . . . . . . . 290 10.2 Nonmonotonic logics kd45 and Sw5 296 10.3 Autoepistemic logic; context semantics 308 lOA Comments and remarks . . . . . . . . . 315 11 Topics in modal nonmonotonic logic 317 11.1 Algorithms to compute S-expansions 317 XII Table of Contents 11.2 Monotonic modal logics with the same nonmonotonic counter- part . . . . . . . . . . . . . . . . . 325 11.3 Adding new definitions to a theory 337 11.4 Bounding the depth of introspection 341 11.5 Ground S-expansions. . . . . . . . . 343 11.6 Bounding introspection to £ U {.....,Lcp: cp E £} 346 11.7 Comments and remarks . . . . . . . . 350 12 Relations among nonmonotonic formalisms 351 12.1 Expressing default reasoning in modal nonmonotonic logics 351 12.2 Another semantics for default logic . . . . . . . . . . . . . 357 12.3 Interpreting logic programs in modal nonmonotonic logics 362 12.4 More characterizations of stable answer sets . . . . . . . . 364 12.5 Weak extensions, stable expansions and supported models 368 12.6 Interpreting logic programs in autoepistemic logic. 374 12.7 Truth maintenance and nonmonotonic systems 376 12.8 Comments and remarks . . . . . . . . . . . . . 380 13 Complexity of some forms of nonmonotonic reasoning 383 13.1 Basic notions of the complexity theory 383 13.2 Complexity of default reasoning. . . . 385 13.3 Complexity of reasoning with modal nonmonotonic logics 391 13.4 Complexity issues for finite logic programs . . . . . . . . 396 13.5 Issues in complexity of models of infinite logic programs 399 13.6 Comments and remarks 404 References 405 Index ... 411 List of Figures 3.1 Algorithm for computing BDjw(W) .......... 44 3.2 Algorithm for computing extensions of default heories 85 3.3 Algorithm for computing a candidate theory for an extension, given an ordering of defaults. . . . . . . . . . . . . . . . 86 3.4 Algorithm for computing extensions of default theories . . .. 87 3.5 Algorithm for computing a partial extension of a default theory given an ordering of defaults. . . . . . . . . . . . . . . . . .. 101 4.1 Algorithm for computing all extensions of a normal default theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. 107 7.1 Axiomatizations of some modal logics 197 8.1 Algorithm InStabA 240 8.2 Algorithm InStabB 241 8.3 Algorithm InStabC 246 8.4 Algorithm InStabD 247 11.1 Algorithm IC .... 319 11.2 Algorithm AIL.ExpsA . 320 11.3 Algorithm AILExpsB . 321