In this paper, we introduce the methodology and techniques of meta-argumentation to model argumentation. The methodology of meta-argumentation instantiates Dung’s abstract argumentation theory with an extended argumentation theory, and is thus based on a combination of the methodology of instantiating abstract arguments, and the methodology of extending Dung’s basic argumentation frameworks with other relations among abstract arguments. The technique of meta-argumentation applies Dung’s theory of abstract argumentation to itself, by instantiating Dung’s abstract arguments with meta-arguments using a technique called flattening. (...) We characterize the domain of instantiation using a representation technique based on soundness and completeness. Finally, we distinguish among various instantiations using the technique of specification languages. (shrink)

In this paper we suggest adding to predicate modal and temporal logic a locality predicate W which gives names to worlds (or time points). We also study an equal time predicate D(x, y)which states that two time points are at the same distance from the root. We provide the systems studied with complete axiomatizations and illustrate the expressive power gained for modal logic by simulating other logics. The completeness proofs rely on the fairly intuitive notion of a configuration in order (...) to use a proof technique similar to a Henkin completion mixed with a tableau construction. The main elements of the completeness proofs are given for each case, while purely technical results are grouped in the appendix. (shrink)

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, 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. (shrink)

The purpose of this paper is to communicate some developments in what we call the new logic. In a nutshell the new logic is a model of the behaviour of a logical agent. By these lights, logical theory has two principal tasks. The first is an account of what a logical agent is. The second is a description of how this behaviour is to be modelled. Before getting on with these tasks we offer a disclaimer and a warning. The disclaimer (...) is that although the new logic is significantly different from it, we have no inclination to see the new logic as a rival of mathematical logic. We do not advocate the displacement of, e.g. model theory, but rather its supplementation or adaptation. The warning is that, whereas mathematical logic must eschew psychologism, the new logic cannot do without it. The fuller story of the new logic must eschew psychologism, the new logic cannot do without it. The fuller story of the new logic is part of our book, The Reach of Abduction, scheduled to appear in 2001 or early 2002. (shrink)

Modal logics, originally conceived in philosophy, have recently found many applications in computer science, artificial intelligence, the foundations of mathematics, linguistics and other disciplines. Celebrated for their good computational behaviour, modal logics are used as effective formalisms for talking about time, space, knowledge, beliefs, actions, obligations, provability, etc. However, the nice computational properties can drastically change if we combine some of these formalisms into a many-dimensional system, say, to reason about knowledge bases developing in time or moving objects. To study (...) the computational behaviour of many-dimensional modal logics is the main aim of this book. On the one hand, it is concerned with providing a solid mathematical foundation for this discipline, while on the other hand, it shows that many seemingly different applied many-dimensional systems (e.g., multi-agent systems, description logics with epistemic, temporal and dynamic operators, spatio-temporal logics, etc.) fit in perfectly with this theoretical framework, and so their computational behaviour can be analyzed using the developed machinery. We start with concrete examples of applied one- and many-dimensional modal logics such as temporal, epistemic, dynamic, description, spatial logics, and various combinations of these. Then we develop a mathematical theory for handling a spectrum of 'abstract' combinations of modal logics - fusions and products of modal logics, fragments of first-order modal and temporal logics - focusing on three major problems: decidability, axiomatizability, and computational complexity. Besides the standard methods of modal logic, the technical toolkit includes the method of quasimodels, mosaics, tilings, reductions to monadic second-order logic, algebraic logic techniques. Finally, we apply the developed machinery and obtained results to three case studies from the field of knowledge representation and reasoning: temporal epistemic logics for reasoning about multi-agent systems, modalized description logics for dynamic ontologies, and spatio-temporal logics. The genre of the book can be defined as a research monograph. It 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). On the other hand, well-known results from modal and first-order logic are formulated without proofs and supplied with references to accessible sources. The intended audience of this book is logicians as well as those researchers who use logic in computer science and artificial intelligence. More specific application areas are, e.g., knowledge representation and reasoning, in particular, terminological, temporal and spatial reasoning, or reasoning about agents. And we also believe that researchers from certain other disciplines, say, temporal and spatial databases or geographical information systems, will benefit from this book as well. Key Features: Integrated approach to modern modal and temporal logics and their applications in artificial intelligence and computer science Written by internationally leading researchers in the field of pure and applied logic Combines mathematical theory of modal logic and applications in artificial intelligence and computer science Numerous open problems for further research Well illustrated with pictures and tables. (shrink)

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. (shrink)

This paper is intended first for the formal argumentation community (see https://comma.csc.liv.ac.uk/). This community develops logics and systems modelling argumentation and dialogues. The community is in search of major applications areas for their models. One such application area e.g. is Law. The message of this paper is that there is another major application area for formal argumentation. There is an international community of sex offender therapist that is well established and well funded, and their therapy methods use (methods that can (...) be modelled by) formal argumentation and logic. This community presents a natural application area for formal argumentation. We thus describe in this paper how the sex offender therapists work, to give the formal argumentation researcher a view of this application area. What is especially important about this application area is that in order to model it and learn from it, the formal argumentation community have to evolve their formal methods and adapt to this new application. Part of this enhancement is to modify and import certain methods from other areas of Logic e.g. from Non-Monotonic logic. The members of the formal argumentation community are not familiar, on average, with other areas of logic, and so we also describe in this paper, what we need from neighbouring logics. This makes this paper of interest also to sex offender therapist as well. They may be already familiar with their own practices, but the additional logics described will be of interest to them. (shrink)

The traditional Dung networks depict arguments as atomic and study the relationships of attack between them. This can be generalised in two ways. One is to consider various forms of attack, support, feedback, etc. Another is to add content to nodes and put there not just atomic arguments but more structure, e.g. proofs in some logic or simply just formulas from a richer language. This paper offers to use temporal and modal language formulas to represent arguments in the nodes of (...) a network. The suitable semantics for such networks is Kripke semantics. We also introduce a new key concept of usability of an argument. This is the beginning of a continuing research for adding contents to the nodes of an argumentation network. This research will allow us to address notions like ?what does it exactly mean for a node to attack another? or ?what does it mean for a network to be consistent? or ?can we give proper proof rules to manipulate networks?, and more. (shrink)

In this work we develop goal-directed deduction methods for the implicational fragment of several modal logics. We give sound and complete procedures for strict implication of K, T, K4, S4, K5, K45, KB, KTB, S5, G and for some intuitionistic variants. In order to achieve a uniform and concise presentation, we first develop our methods in the framework of Labelled Deductive Systems [Gabbay 96]. The proof systems we present are strongly analytical and satisfy a basic property of cut admissibility. (...) We then show that for most of the systems under consideration the labelling mechanism can be avoided by choosing an appropriate way of structuring theories. One peculiar feature of our proof systems is the use of restart rules which allow to re-ask the original goal of a deduction. In case of K, K4, S4 and G, we can eliminate such a rule, without loosing completeness. In all the other cases, by dropping such a rule, we get an intuitionistic variant of each system. The present results are part of a larger project of a goal directed proof theory for non-classical logics; the purpose of this project is to show that most implicational logics stem from slight variations of a unique deduction method, and from different ways of structuring theories. Moreover, the proof systems we present follow the logic programming style of deduction and seem promising for proof search [Gabbay and Reyle 84, Miller et al. 91]. (shrink)

This is a handbook, written by a number of authors from different research communities. Even though the subject matter of the book is reasonably unified, the divergence between their communities – firstly category theory and type theory, secondly universal algebra, and thirdly classical logic and complexity theory -- makes it difficult to get an overview; these communities are notorious for their poor relations with each other. Thus, even though it would be tempting to envisage a world in which the various (...) chapters would be written so as to illuminate each other, and in which prospective readers would have a broad enough background to be able to appreciate all of this book, it is not the world that we live in. (shrink)

We are used to the idea that computers operate on numbers, yet another kind of data is equally important: the syntax of formal languages, with variables, binding, and alpha-equivalence. The original application of nominal techniques, and the one with greatest prominence in this paper, is to reasoning on formal syntax with variables and binding. Variables can be modelled in many ways: for instance as numbers (since we usually take countably many of them); as links (since they may `point' to a (...) binding site in the term, where they are bound); or as functions (since they often, though not always, represent `an unknown'). None of these models is perfect. In every case for the models above, problems arise when trying to use them as a basis for a fully formal mechanical treatment of formal language. The problems are practical—but their underlying cause may be mathematical. The issue is not whether formal syntax exists, since clearly it does, so much as what kind of mathematical structure it is. To illustrate this point by a parody, logical derivations can be modelled using a Gödel encoding (i.e., injected into the natural numbers). It would be false to conclude from this that proof-theory is a branch of number theory and can be understood in terms of, say, Peano's axioms. Similarly, as it turns out, it is false to conclude from the fact that variables can be encoded e.g., as numbers, that the theory of syntax-with-binding can be understood in terms of the theory of syntax-without-binding, plus the theory of numbers (or, taking this to a logical extreme, purely in terms of the theory of numbers). It cannot; something else is going on. What that something else is, has not yet been fully understood. In nominal techniques, variables are an instance of names, and names are data. We model names using urelemente with properties that, pleasingly enough, turn out to have been investigated by Fraenkel and Mostowski in the first half of the 20th century for a completely different purpose than modelling formal language. What makes this model really interesting is that it gives names distinctive properties which can be related to useful logic and programming principles for formal syntax. Since the initial publications, advances in the mathematics and presentation have been introduced piecemeal in the literature. This paper provides in a single accessible document an updated development of the foundations of nominal techniques. This gives the reader easy access to updated results and new proofs which they would otherwise have to search across two or more papers to find, and full proofs that in other publications may have been elided. We also include some new material not appearing elsewhere. (shrink)

This text centers around three main subjects. The first is the concept of modularity and independence in classical logic and nonmonotonic and other nonclassical logic, and the consequences on syntactic and semantical interpolation and language change. In particular, we will show the connection between interpolation for nonmonotonic logic and manipulation of an abstract notion of size. Modularity is essentially the ability to put partial results achieved independently together for a global result. The second aspect of the book is the authors' (...) uniform picture of conditionals, including many-valued logics and structures on the language elements themselves and on the truth value set. The third topic explained by the authors is neighbourhood semantics, their connection to independence, and their common points and differences for various logics, e.g., for defaults and deontic logic, for the limit version of preferential logics, and for general approximation"--Publisher. (shrink)

In this paper we explore a generalization of traditional abduction which can simultaneously perform two different tasks: given an unprovable sequent Γ ⊢ G, find a sentence H such that Γ, H ⊢ G is provable ; given a provable sequent Γ ⊢ G, find a sentence H such that Γ ⊢ H and the proof of Γ, H ⊢ G is simpler than the proof of Γ ⊢ G . We argue that the two tasks should not be distinguished, (...) and present a general procedure for finding suitable hypotheses or lemmas. When the original sequent is provable, the abduced formula can be seen as a cut formula with respect to Gentzen's sequent calculus, so the abduction method is cut-based. Our method is based on the tableau-like system KE and we argue for its advantages over existing abduction methods based on traditional Smullyan-style Tableaux. (shrink)

Formal models of argumentation have been investigated in several areas, from multi-agent systems and artificial intelligence (AI) to decision making, philosophy and law. In artificial intelligence, logic-based models have been the standard for the representation of argumentative reasoning. More recently, the standard logic-based models have been shown equivalent to standard connectionist models. This has created a new line of research where (i) neural networks can be used as a parallel computational model for argumentation and (ii) neural networks can be used (...) to combine argumentation, quantitative reasoning and statistical learning. At the same time, non-standard logic models of argumentation started to emerge. In this paper, we propose a connectionist cognitive model of argumentation that accounts for both standard and non-standard forms of argumentation. The model is shown to be an adequate framework for dealing with standard and non-standard argumentation, including joint-attacks, argument support, ordered attacks, disjunctive attacks, meta-level attacks, self-defeating attacks, argument accrual and uncertainty. We show that the neural cognitive approach offers an adequate way of modelling all of these different aspects of argumentation. We have applied the framework to the modelling of a public prosecution charging decision as part of a real legal decision making case study containing many of the above aspects of argumentation. The results show that the model can be a useful tool in the analysis of legal decision making, including the analysis of what-if questions and the analysis of alternative conclusions. The approach opens up two new perspectives in the short-term: the use of neural networks for computing prevailing arguments efficiently through the propagation in parallel of neuronal activations, and the use of the same networks to evolve the structure of the argumentation network through learning (e.g. to learn the strength of arguments from data). (shrink)

This study examines BDI logics in the context of Gabbay's fibring semantics. We show that dovetailing can be adopted as a semantic methodology to combine BDI logics. We develop a set of interaction axioms that can capture static as well as dynamic aspects of the mental states in BDI systems, using Catach's incestual schema G^[a, b, c, d]. Further we exemplify the constraints required on fibring function to capture the semantics of interactions among modalities. The advantages of having a (...) fibred approach is discussed in the final section. (shrink)

This paper introduces a generalization of Reiter’s notion of “extension” for default logic. The main difference from the original version mainly lies in the way conflicts among defaults are handled: in particular, this notion of “general extension” allows defaults not explicitly triggered to pre-empt other defaults. A consequence of the adoption of such a notion of extension is that the collection of all the general extensions of a default theory turns out to have a nontrivial algebraic structure. This fact has (...) two major technical fall-outs: first, it turns out that every default theory has a general extension; second, general extensions allow one to define a well-behaved, skeptical relation of defeasible consequence for default theories, satisfying the principles of Reflexivity, Cut, and Cautious Monotonicity formulated by D. Gabbay. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:April 3, 2010 (11:17 am) C:\Users\Milt\Desktop\backup copy of Ken's G\WPData\TYPE2902\russell 29,2 050 red.wpd 1 Gabbay and Woods, eds., The Rise of Modern Logic from Leibniz to Frege, Vol. 3 of the Handbook of the History of Logic (Amsterdam, etc.: North-Holland, 2004). russell: the Journal of Bertrand Russell Studies n.s. 29 (winter 2009–10): 167–90 The Bertrand Russell Research Centre, McMaster U. issn 0036-01631; online 1913-8032 eviews BERTRAND RUSSELL IN (...) RECENT BOOKS ON LOGIC HISTORY Irving Anellis Peirce Edition / Indiana U.–Purdue U. Indianapolis, in 46202–5157, usa [email protected] Dov M. Gabbay and John Woods, eds. Logic from Russell to Church. Vol. 5 of The Handbook of the History of Logic. Amsterdam, etc.: North-Holland, 2009. Pp. xii + 1056. us$260; £157.99; ¤185.95. Leila Haaparanta, ed. The Development of Modern Logic. Oxford and New York: Oxford U. P., 2009. Pp. x + 904. us$150.00. The essay “Bertrand Russell’s Logic” by Andrew D. Irvine in Volume 5 of the Handbook of the History of Logic is one of the shortest in the volume (pp. 1–28). But something of Russell pervades many of the other essays as well, as we might expect given the centrality that Principia Mathematica has occupied in the historiography of logic through much of the twentieth century. This is especially evident in the lengthiest of the essays, Andrea Cantini’s “Paradoxes, Self-reference and Truth in the 20th Century” (pp. 875–1013), and more than tangentially in Dale Jacquette’s “Logic for Meinongian Object Theory Semantics” (pp. 29–76) and Michael Potter’s “The Logic of the Tractatusz” (pp. 255–304). In their preface, the editors of the Handbook explain (p. vii) the rationale for treating Frege and Russell in separate volumes.1 One reason is that it was a matter of simple conveniencez—zto keep the volume covering logic from Leibniz to Frege of manageable size. The other is historical: while admitting that Frege and Russell shared important goals and the philosophical position of logicism, it is noted that Frege’s most important work in logic and foundations was carried out prior to his learning of Russell’s paradox, whereas the entire corpus of Russell’s work, Principiaz included, was designed to a considerable extent in eTorts to deal with the paradox, as was much of the work in logic, set theory, and philosophy of logic that came as a consequence of the discovery of that paradox. Gabbay April 3, 2010 (11:17 am) C:\Users\Milt\Desktop\backup copy of Ken's G\WPData\TYPE2902\russell 29,2 050 red.wpd 168 Reviews and Woods also make explicit the philosophical diTerences between Frege and Russell regarding the epistemological status of axioms as one of the signiWcant diTerences between these two. More particularly, the editors assert (p. viii) that, in the very brief period between publication of the second volume of Frege’s Grundgesetze (1903) and Russell’s Principles of Mathematics (1903), there was a pronounced shift initiated in the goals of mathematical logic, away from naïve apriority of axiom systems, towards study of the limits and properties of formal systems.Thecontributors to these metalogical concerns, Herbrand, Hilbert, and Gödel, among others, are the subject of the bulk of the essays included in Volume 5 of the Handbook. The task that Irvine undertakes is initiated by the eTort to understand the unity of Russell’s technical body of work in mathematics, logic, metaphysics, and epistemology. Thus the discrepancy between the neo-Hegelian concept of relations, inherited from Bradley, with certain types of relationsz—zlogical, spatial, temporal, for examplez—zwith the mathematical understanding of relations, is given as the ground for Russell’s abandonment of idealism in favour of realism (pp. 4–5). For example, there is nothing inherent in two relata, say Abelard and Héloise, which contributes to the relation of love between the pair; rather, its root is found in the mental states of one or the other of the lovers, so that the relation itself is not an intrinsic property of one of the pair. Likewise, Russell reaches this position... (shrink)

This paper investigates modular combinations of temporal logic systems. Four combination methods are described and studied with respect to the transfer of logical properties from the component one-dimensional temporal logics to the resulting combined two-dimensional temporal logic. Three basic logical properties are analyzed, namely soundness, completeness, and decidability. Each combination method comprises three submethods that combine the languages, the inference systems, and the semantics of two one-dimensional temporal logic systems, generating families of two-dimensional temporal languages with varying expressivity and varying (...) degrees of transfer of logical properties. The temporalization method and the independent combination method are shown to transfer all three basic logical properties. The method of full join of logic systems generates a considerably more expressive language but fails to transfer completeness and decidability in several cases. So a weaker method of restricted join is proposed and shown to transfer all three basic logical properties. (shrink)

We show that Gabbay’s nonmonotonic consequence relations c an be reduced to a new family of relations, called entrenchment relations. Entrenchment relations provide a direct generalization of epistemic entrenchment and expectation ordering introduced by G ̈ardenfors and Makinson for the study of belief revision and expectation inference, respectively.

We study some operations that may be defined using the minimum operator in the context of a Heyting algebra. Our motivation comes from the fact that 1) already known compatible operations, such as the successor by Kuznetsov, the minimum dense by Smetanich and the operation G by Gabbay may be defined in this way, though almost never explicitly noted in the literature; 2) defining operations in this way is equivalent, from a logical point of view, to two clauses, one (...) corresponding to an introduction rule and the other to an elimination rule, thus providing a manageable way to deal with these operations. Our main result is negative: all operations that arise turn out to be Heyting terms or the mentioned already known operations or operations interdefinable with them. However, it should be noted that some of the operations that arise may exist even if the known operations do not. We also study the extension of Priestley duality to Heyting algebras enriched with the new operations. (shrink)

This book is a specialized monograph on the development of the mathematical and computational metatheory of reductive logic and proof-search, areas of logic that are becoming important in computer science. A systematic foundational text on these emerging topics, it includes proof-theoretic, semantic/model-theoretic and algorithmic aspects. The scope ranges from the conceptual background to reductive logic, through its mathematical metatheory, to its modern applications in the computational sciences. Suitable for researchers and graduate students in mathematical, computational and philosophical logic, and in (...) theoretical computer science and artificial intelligence, this is the latest in the prestigous world-renowned Oxford Logic Guides, which contains Michael Dummet's Elements of intuitionism (2nd Edition), Dov M. Gabbay, Mark A. Reynolds, and Marcelo Finger's Temporal Logic Mathematical Foundations and Computational Aspects, 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, and P. T. Johnstone's Sketches of an Elephant: A Topos Theory Compendium: Volumes 1 and 2. (shrink)

This book is a specialized monograph on the development of the mathematical and computational metatheory of reductive logic and proof-search, areas of logic that are becoming important in computer science. A systematic foundational text on these emerging topics, it includes proof-theoretic, semantic/model-theoretic and algorithmic aspects. The scope ranges from the conceptual background to reductive logic, through its mathematical metatheory, to its modern applications in the computational sciences. Suitable for researchers and graduate students in mathematical, computational and philosophical logic, and in (...) theoretical computer science and artificial intelligence, this is the latest in the prestigous world-renowned Oxford Logic Guides, which contains Michael Dummet's Elements of intuitionism, Dov M. Gabbay, Mark A. Reynolds, and Marcelo Finger's Temporal Logic Mathematical Foundations and Computational Aspects, 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, and P. T. Johnstone's Sketches of an Elephant: A Topos Theory Compendium: Volumes 1 and 2. (shrink)

We study some operations that may be defined using the minimum operator in the context of a Heyting algebra. Our motivation comes from the fact that 1) already known compatible operations, such as the successor by Kuznetsov, the minimum dense by Smetanich and the operation G by Gabbay may be defined in this way, though almost never explicitly noted in the literature; 2) defining operations in this way is equivalent, from a logical point of view, to two clauses, one (...) corresponding to an introduction rule and the other to an elimination rule, thus providing a manageable way to deal with these operations. Our main result is negative: all operations that arise turn out to be Heyting terms or the mentioned already known operations or operations interdefinable with them. However, it should be noted that some of the operations that arise may exist even if the known operations do not. We also study the extension of Priestley duality to Heyting algebras enriched with the new operations. (shrink)

Intensional logic has emerged, since the 1960' s, as a powerful theoretical and practical tool in such diverse disciplines as computer science, artificial intelligence, linguistics, philosophy and even the foundations of mathematics. The present volume is a collection of carefully chosen papers, giving the reader a taste of the frontline state of research in intensional logics today. Most papers are representative of new ideas and/or new research themes. The collection would benefit the researcher as well as the student. This book (...) is a most welcome addition to our series. The Editors CONTENTS PREFACE IX JOHAN VAN BENTHEM AND NATASHA ALECHINA Modal Quantification over Structured Domains PATRICK BLACKBURN AND WILFRIED MEYER-VIOL Modal Logic and Model-Theoretic Syntax 29 RUY J. G. B. DE QUEIROZ AND DOV M. GABBAY The Functional Interpretation of Modal Necessity 61 VLADIMIR V. RYBAKOV Logics of Schemes for First-Order Theories and Poly-Modal Propositional Logic 93 JERRY SELIGMAN The Logic of Correct Description 107 DIMITER VAKARELOV Modal Logics of Arrows 137 HEINRICH WANSING A Full-Circle Theorem for Simple Tense Logic 173 MICHAEL ZAKHARYASCHEV Canonical Formulas for Modal and Superintuitionistic Logics: A Short Outline 195 EDWARD N. ZALTA 249 The Modal Object Calculus and its Interpretation NAME INDEX 281 SUBJECT INDEX 285 PREFACE Intensional logic has many faces. In this preface we identify some prominent ones without aiming at completeness. (shrink)

The aim of this work is to develop a declarative semantics for N-Prolog with negation as failure. N-Prolog is an extension of Prolog proposed by Gabbay and Reyle, which allows for occurrences of nested implications in both goals and clauses. Our starting point is an operational semantics of the language defined by means of top-down derivation trees. Negation as finite failure can be naturally introduced in this context. A goal-G may be inferred from a database if every top-down derivation (...) of G from the database finitely fails, i.e., contains a failure node at finite height.Our purpose is to give a logical interpretation of the underlying operational semantics. In the present work we take into consideration only the basic problems of determining such an interpretation, so that our analysis will concentrate on the propositional case. Nevertheless we give an intuitive account of how to extend our results to a first order language. A full treatment of N-Prolog with quantifiers will be deferred to the second part of this work. (shrink)