Dov M. Gabbay

Quantification and modalities have always been topics of great interest for logicians. These two themes emerged from philosophy andlanguage in ancient times; they were studied by traditional informalmethods until the 20th century. In the last century the tools becamehighly mathematical, and both modal logic and quantification found numerous applications in Computer Science. At the same time many other kinds of nonclassical logics were investigated and applied to Computer Science. Although there exist several good books in propositional modal logics, this book is the first detailed monograph in nonclassical first-order quantification. It includes results obtained during the past thirty years. The field is very large, so we confine ourselves with only two kinds of logics: modal and superintuitionistic. The main emphasis of Volume 1 is model-theoretic, and it concentrates on descriptions of different sound semantics and completeness problem --- even for these seemingly simple questions we have our hands full. The major part of the presented material has never been published before. Some results are very recent, and for other results we either give new proofs or first proofs in full detail.

Fuzzy logics are many-valued logics that are well suited to reasoning in the context of vagueness. They provide the basis for the wider field of Fuzzy Logic, encompassing diverse areas such as fuzzy control, fuzzy databases, and fuzzy mathematics. This book provides an accessible and up-to-date introduction to this fast-growing and increasingly popular area. It focuses in particular on the development and applications of "proof-theoretic" presentations of fuzzy logics; the result of more than ten years of intensive work by researchers in the area, including the authors. In addition to providing alternative elegant presentations of fuzzy logics, proof-theoretic methods are useful for addressing theoretical problems (including key standard completeness results) and developing efficient deduction and decision algorithms. Proof-theoretic presentations also place fuzzy logics in the broader landscape of non-classical logics, revealing deep relations with other logics studied in Computer Science, Mathematics, and Philosophy. The book builds methodically from the semantic origins of fuzzy logics to proof-theoretic presentations such as Hilbert and Gentzen systems, introducing both theoretical and practical applications of these presentations.

Humans are often extraordinary at performing practical reasoning. There are cases where the human computer, slow as it is, is faster than any artificial intelligence system. Are we faster because of the way we perceive knowledge as opposed to the way we represent it? The authors address this question by presenting neural network models that integrate the two most fundamental phenomena of cognition: our ability to learn from experience, and our ability to reason from what has been learned. This book is the first to offer a self-contained presentation of neural network models for a number of computer science logics, including modal, temporal, and epistemic logics. By using a graphical presentation, it explains neural networks through a sound neural-symbolic integration methodology, and it focuses on the benefits of integrating effective robust learning with expressive reasoning capabilities. The book will be invaluable reading for academic researchers, graduate students, and senior undergraduates in computer science, artificial intelligence, machine learning, cognitive science and engineering. It will also be of interest to computational logicians, and professional specialists on applications of cognitive, hybrid and artificial intelligence systems.

Starting with simple examples showing the relevance of cutting and pasting logics, the monograph develops a mathematical theory of combining and decomposing logics, ranging from propositional and first-order based logics to higher-order based logics as well as to non-truth functional logics. The theory covers mechanisms for combining semantic structures and deductive systems either of the same or different nature (for instance, two Hilbert calculi or a Hilbert calculus and a tableau calculus). The important issue of preservation of properties is extensively addressed. For instance, sufficient conditions are provided for a combined logic to be sound and complete when the original component logics are known to be sound and complete. The book brings the reader to the front line of current research in the field by showing both recent achievements and directions of future investigations (in particular, multiple open problems). It also provides examples of potential applications in emergent fields like security protocols, quantum computing, networks and argumentation theory, besides discussing more classical applications like software specification, knowledge representation, computational linguistics and modular automated reasoning. This monograph will be of interest to researchers and graduate students in mathematical logic, theory of computation and philosophical logic with no previous knowledge of the subject of combining and decomposing logics, but with a working knowledge of first-order logic. The book will also be relevant for people involved in research projects where logic is used as a tool and the need for working with several logics at the same time is mandatory (for instance, temporal, epistemic and probabilistic logics).

This book is a specialized monograph on interpolation and definability, a notion central in pure logic and with significant meaning and applicability in all areas where logic is applied, especially computer science, artificial intelligence, logic programming, philosophy of science and natural language. Suitable for researchers and graduate students in mathematics, computer science and philosophy, this is the latest in the prestigous world-renowned Oxford Logic Guides, which contains Michael Dummet's Elements of intuitionism (second edition), J. M. Dunn and G. Hardegree's Algebraic Methods in Philosophical Logic, H. Rott's Change, Choice and Inference: A Study of Belief Revision and Nonmonotonic Reasoning, P. T. Johnstone's Sketches of an Elephant: A Topos Theory Compendium: Volumes 1 and 2, and David J. Pym and Eike Ritter's Reductive Logic and Proof Search: Proof theory, semantics and control.

The present work is a continuation of the authors' acclaimed multi-volume A Practical Logic of Cognitive Systems. After having investigated the notion of relevance in their previous volume, Gabbay and Woods now turn to abduction. In this highly original approach, abduction is construed as ignorance-preserving inference, in which conjecture plays a pivotal role. Abduction is a response to a cognitive target that cannot be hit on the basis of what the agent currently knows. The abducer selects a hypothesis which were it true would enable the reasoner to attain his target. He concludes from this fact that the hypothesis may be conjectured. In allowing conjecture to stand in for the knowledge he fails to have, the abducer reveals himself to be a satisficer, since an abductive solution is not a solution from knowledge. Key to the authors' analysis is the requirement that a conjectured proposition is not just what a reasoner might allow himself to assume, but a proposition he must defeasibly release as a premiss for further inferences in the domain of enquiry in which the original abduction problem has arisen. The coverage of the book is extensive, from the philosophy of science to computer science and AI, from diagnostics to the law, from historical explanation to linguistic interpretation. One of the volume's strongest contributions is its exploration of the abductive character of criminal trials, with special attention given to the standard of proof beyond a reasonable doubt. Underlying their analysis of abductive reasoning is the authors' conception of practical agency. In this approach, practical agency is dominantly a matter of the comparative modesty of an agent's cognitive agendas, together with comparatively scant resources available for their advancement. Seen in these ways, abduction has a significantly practical character, precisely because it is a form of inference that satisfices rather than maximizes its response to the agent's cognitive target. The Reach of Abduction will be necessary reading for researchers, graduate students and senior undergraduates in logic, computer science, AI, belief dynamics, argumentation theory, cognitive psychology and neuroscience, linguistics, forensic science, legal reasoning and related areas. Key features: - Reach of Abduction is fully integrated with a background logic of cognitive systems. - The most extensive coverage compared to competitive works. - Demonstrates not only that abduction is a form of ignorance preserving inference but that it is a mode of inference that is wholly rational. - Demonstrates the satisficing rather than maximizing character of abduction. - The development of formal models of abduction is considerably more extensive than one finds in existing literature. It is an especially impressive amalgam of sophisticated conceptual analysis and extensive logical modelling.

Artificial Intelligence is concerned with producing devices that help or replace human beings in their daily activities. Neural-symbolic learning systems play a central role in this task by combining, and trying to benefit from, the advantages of both the neural and symbolic paradigms of artificial intelligence. This book provides a comprehensive introduction to the field of neural-symbolic learning systems, and an invaluable overview of the latest research issues in this area. It is divided into three sections, covering the main topics of neural-symbolic integration - theoretical advances in knowledge representation and learning, knowledge extraction from trained neural networks, and inconsistency handling in neural-symbolic systems. Each section provides a balance of theory and practice, giving the results of applications using real-world problems in areas such as DNA sequence analysis, power systems fault diagnosis, and software requirements specifications. Neural-Symbolic Learning Systems will be invaluable reading for researchers and graduate students in Engineering, Computing Science, Artificial Intelligence, Machine Learning and Neurocomputing. It will also be of interest to Intelligent Systems practitioners and anyone interested in applications of hybrid artificial intelligence systems.

This ground-breaking volume sets out an original model of the dynamics of language processing, which can be used to explain the structural properties of language in a simple and elegant way. The model is introduced both informally and formally, and is applied to a range of languages.

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 generalization of the logic programming style of deduction, and it is particularly favourable for proof search. The methodology is applied for the first time in a uniform way to a wide range of non-classical systems, covering intuitionistic, intermediate, modal and substructural logics. The book can also be used as an introduction to these logical systems form a procedural perspective. Readership: Computer scientists, mathematicians and philosophers, and anyone interested in the automation of reasoning based on non-classical logics. The book is suitable for self study, its only prerequisite being some elementary knowledge of logic and proof theory.

This is the second volume of this respected work in temporal logic. Whereas volume 1 dealt primarily with basic concepts and methods, volume 2 discusses the more applicable aspects of temporal logics. The first four chapters continue the more theoretical presentations in volume 1, covering automata, branching time and labelled deduction. The rest of the book discusses temporal databases, temporal execution and programming, actions and planning.

Modern applications of logic, in mathematics, theoretical computer science, and linguistics, require combined systems involving many different logics working together. In this book the author offers a basic methodology for combining-or fibring-systems. This means that many existing complex systems can be broken down into simpler components, hence making them much easier to manipulate. Using this methodology the book discusses ways of obtaining a wide variety of multimodal, modal intuitionistic, modal substructural and fuzzy systems in a uniform way. It also covers self-fibred languages which allow formulae to apply to themselves. The book also studies sufficient conditions for transferring properties of the component logics into properties of the combined system.

This important book provides a new unifying methodology for logic. It replaces the traditional view of logic as manipulating sets of formulas by the notion of structured families of labelled formulas, the labels having algebraic structure. This simple device has far reaching consequences for the methodology of logics and their semantics. The book studies the main features of such systems as well as many applications. The framework of Labelled Deductive Systems is of interest to a large variety of readers. At one extreme there is the pure mathematical logician who likes exact formal definitions and dry theorems, who probably specializes in one logic and methodology. At the other extreme there is the practical consumer of logic, who likes to absorb the intutions and use labelling as needed to advance the cause of applications. The book begins with an intuitive presentation of LDS in the context of traditional current views of monotonic and nonmonotonic logics. It is less orientated towards the pure logician and more towards the practical consumer of logic. The main part of the book presents the formal theory of LDS for the formal logician. The author has tried to avoid the style of definition-lemma-theorem and has put in some explanation.

This long awaited book gives a thorough account of the mathematical foundations of Temporal Logic, one of the most important areas of logic in computer science. The book, which consists of fifteen chapters, moves on from giving a solid introduction in semantical and axiomatic approaches to temporal logic to covering the central topics of predicate temporal logic, meta-languages, general theories of axiomatization, many dimensional systems, propositional quantifiers, expressive power, Henkin dimension, temporalization of other logics, and decidability results. Much of the research presented here is frontline in the new results and in the unifying methodology. This is an indispensable reference work for both the pure logician and the theoretical computer scientist.

Logic is now widely recognized to be one of the foundational disciplines of computing and has found applications in virtually all aspects of the subject, from software engineering and hardware to programming languages and artificial intelligence. There is a growing need for an in-depth survey of the applications of logic in Al and computer science. The Handbook of Logic in Articial Intelligence and Logic Programming and its companion, the Handbook of Logic in Computer Science, have been created in response to this need. We see the creation of the Handbook as a combination of authoritative exposition, comprehensive survey, and fundamental research exploring the underlying themes in the various areas. The intended audience is graduate students and researchers in the areas of A1 and logic, as well as other people interested in the subject. We assume as background some mathematical sophistication. Much of the material will be of interest to logicians and mathematicians. The tables of contents of the volumes were finalized after extensive discussions between handbook authors and second readers. The first volumes present the logical foundations and deduction methodologies extensively used in AI. Volumes 3 and 4 cover reasoning, and Volume 5 details logic programming. The chapters, which in many cases are of monograph length and scope, emphasize possible unifying themes. They are written by internationally renowned researchers in the respective areas. The chapters are co-ordinated and their contents have been reviewed in joint meetings.

Logic is now widely recognized to be one of the foundational disciplines of computing and has found applications in virtually all aspects of the subject, from software engineering and hardware to programming languages and artificial intelligence. There is a growing need for an in-depth survey of the applications in logic in A1 and computer science. The Handbook of Logic in Ariticial Intelligence and Logic Programming and its companion, the Handbook of Logic in Computer Science, have been created in response to this need. We see the creation of the Handbook as a combination of authoritative exposition, comprehensive survey, and fundamental research exploring the underlying themes in the various areas. The intended audience is graduate students and researchers in the areas of A1 and logic, as well as other people interested in the subject. We assume as background some mathematical sophistication. Much of the material will be of interest to logicians and mathematicians. The tables of contents of the volumes were finalized after extensive discussions between handbook authors and second readers. The first volumes present the logical foundations and deduction methodologies extensively used in A1. Volumes 3 and 4 cover reasoning, and Volume 5 details logic programming. The chapters which in many cases are of monograph length and scope, emphasize possible unifying themes. They are written by internationally renowned researchers in the respective areas. The chapters are co-ordinated and their contents have been reviewed in joint meetings.

Logic is now widely recognized to be one of the foundational disciplines of computing and has found applications in virtually all aspects of the subject, from software engineering and hardware to programming languages and artificial intelligence. This Handbook has been created in response to the growing need for an in-depth survey of the applications of logic in AI and computer science. The Handbook of Logic in Artificial Intelligence and Logic Programming will be published in five volumes. Each volume provides a combination of authoritative exposition, comprehensive survey, and fundamental research exploring the underlying unifying themes in the various areas. this first volume presents the logical foundations and deduction methodologies extensively used in AI.

From the point of view of non-classical logics, Heyting's implication is the smallest implication for which the deduction theorem holds. This book studies properties of logical systems having some of the classical connectives and implication in the neighbourhood of Heyt­ ing's implication. I have not included anything on entailment, al­ though it belongs to this neighbourhood, mainly because of the appearance of the Anderson-Belnap book on entailment. In the later chapters of this book, I have included material that might be of interest to the intuitionist mathematician. Originally, I intended to include more material in that spirit but I decided against it. There is no coherent body of material to include that builds naturally on the present book. There are some serious results on topological models, second order Beth and Kripke models, theories of types, etc., but it would require further research to be able to present a general theory, possibly using sheaves. That would have postponed pUblication for too long. I would like to dedicate this book to my colleagues, Professors G. Kreisel, M. O. Rabin and D. Scott. I have benefited greatly from Professor Kreisel's criticism and suggestions. Professor Rabin's fun­ damental results on decidability and undecidability provided the powerful tools used in obtaining the majority of the results reported in this book. Professor Scott's approach to non-classical logics and especially his analysis of the Scott consequence relation makes it possible to present Heyting's logic as a beautiful, integral part of non-classical logics.

This book is intended to serve as an advanced text and reference work on modal logic, a subject of growing importance which has applications to philosophy and linguistics. Although it is based mainly on research which I carried out during the years 1969-1973, it also includes some related results obtained by other workers in the field (see the refer­ ences in Part 7). Parts 0, 1 and 2, can be used as the basis of a one year graduate course in modal logic. The material which they contain has been taught in such courses at Stanford since 1970. The remaining parts of the book contain more than enough material for a second course in modal logic. The exercises supplement the text and are usually difficult. I wish to thank Stanford University and Bar-Han University for making it possible for me to continue and finish this work, and A. Ungar for correcting the typescript. Bar-Ilan University, Israel Dov M. GABBA Y PART 0 AN INTRODUCTION TO GENERAL INTENSIONAL LOGICS CHAPTER 0 CONSEQUENCE RELATIONS Motivation We introduce the notions of a consequence relation (which is a generalization of the notion of a logical system) and of a semantics. We show that every consequence relation is complete for a canonical semantics. We define the notion of one semantics being Dian in another and study the basic properties of this notion. The concepts of this chapter are generalizations of the various notions of logical system and possible world semantics found in the literature.