Search

Intuitionistic propositional logicInt and its extensions, known as intermediate or superintuitionistic logics, in many respects can be regarded as just fragments of classical modal logics containingS4. The main aim of this paper is to construct a similar correspondence between intermediate logics augmented with modal operators—we call them intuitionistic modal logics—and classical polymodal logics We study the class of intuitionistic polymodal logics in which modal operators satisfy only the congruence rules and so may be treated as various sorts of □ and ◇.

Tense logics formulated in the bimodal propositional language are investigated with respect to Kripke-completeness (completeness) and decidability. It is proved that all minimal tense extensions of modal logics of finite width (in the sense of K. Kine) as well as all minimal tense extensions of cofinal subframe logics (in the sense of M. Zakharyaschev) are complete. The decidability of all finitely axiomatizable minimal tense extensions of cofinal subframe logics is shown. A number of variations and extensions of these results are also presented.

Kripke bundle and C-set semantics are known as semantics which generalize standard Kripke semantics. In [4] and in [1, 2] it is shown that Kripke bundle and C-set semantics are stronger than standard Kripke semantics. Also it is true that C-set semantics for superintuitionistic logics is stronger than Kripke bundle semantics ([6]). Modal predicate logic Q-S4.1 is not Kripke bundle complete ([3] - it is also yielded as a corollary to Theorem 6.1(a) of the present paper). This is shown by using difference of Kripke bundle semantics and C-set semantics. In this paper, by using the same idea we show that incompleteness results in Kripke bundle semantics which are extended versions of [2].

In this paper we provide cut-free tableau calculi for the intuitionistic modal logics IK, ID, IT, i.e. the intuitionistic analogues of the classical modal systems K, D and T. Further, we analyse the necessity of duplicating formulas to which rules are applied. In order to develop these calculi we extend to the modal case some ideas presented by Miglioli, Moscato and Ornaghi for intuitionistic logic. Specifically, we enlarge the language with the new signs Fc and CR near to the usual signs T and F. In this work we establish the soundness and completeness theorems for these calculi with respect to the Kripke semantics proposed by Fischer Servi.

This paper investigates partitions of lattices of modal logics based on superintuitionistic logics which are defined by forming, for each superintuitionistic logic L and classical modal logic Θ, the set L[Θ] of L-companions of Θ. Here L[Θ] consists of those modal logics whose non-modal fragments coincide with L and which axiomatize Θ if the law of excluded middle p V ⌍p is added. Questions addressed are, for instance, whether there exist logics with the disjunction property in L[Θ], whether L[Θ] contains a smallest element, and whether L[Θ] contains lower covers of Θ. Positive solutions as concerns the last question show that there are (uncountably many) superclean modal logics based on intuitionistic logic in the sense of Vakarelov [28]. Thus a number of problems stated in [28] are solved. As a technical tool the paper develops the splitting technique for lattices of modal logics based on superintuitionistic logics and ap plies duality theory from [34].

This papers gives a survey of recent results about simulations of one class of modal logics by another class and of the transfer of properties of modal logics under extensions of the underlying modal language. We discuss: the transfer from normal polymodal logics to their fusions, the transfer from normal modal logics to their extensions by adding the universal modality, and the transfer from normal monomodal logics to minimal tense extensions. Likewise, we discuss simulations of normal polymodal logics by normal monomodal logics, of nominals and the difference operator by normal operators, of monotonic monomodal logics by normal bimodal logics, of polyadic normal modal logics by polymodal normal modal logics, and of intuitionistic modal logics by normal bimodal logics.

Formal aspects of various ways of description of Jan Łukasiewicz’s four-valued modal logic £ are discussed. The original Łukasiewicz’s description by means of the accepted and rejected theorems, together with the four-valued matrix, is presented. Then the improved E.J. Lemmon’s description based upon three specific axioms, together with the relational semantics, is presented as well. It is proved that Lemmon’s axiomatic is not independent: one axiom is derivable on the base of the remanent two. Several axiomatizations, based on three, two or one single axiom are provided and discussed, including S. Kripke’s axiomatics. It is claimed that (a) all substitutions of classical theorems, (b) the rule of modus ponens, (c) the definition of “◊” and (d) the single specific axiom schema: ⬜A ∧ B → A ∧ ⬜B, called the jumping necessity axiom, constitute an elegant axiomatics of the system £.

We provide a general method for generating cut-free and/or analytic hyper sequent Gent Zen-type calculi for a variety of normal modal logics. The method applies to all modal logics characterized by Kripke frames, transitive Kripke frames, or symmetric Kripke frames satisfying some properties, given by first-order formulas of a certain simple form. This includes the logics KT, KD, S4, S5, K4D, K4.2, K4.3, KBD, KBT, and other modal logics, for some of which no Gentzen calculi was presented before. Cut-admissibility (or analyticity in the case of symmetric Kripke frames) is proved semantically in a uniform way for all constructed calculi. The decidability of each modal logic in this class immediately follows.

We consider a general format for sequent rules for not necessarily normal modal logics based on classical or intuitionistic propositional logic and provide relatively simple local conditions ensuring cut elimination for such rule sets. The rule format encompasses e.g. rules for the boolean connectives and transitive modal logics such as S4 or its constructive version. We also adapt the method of constructing suitable rule sets by saturation to the intuitionistic setting and provide a criterium for translating axioms for intuitionistic modal logics into sequent rules. Examples include constructive modal logics and conditional logic \(\mathbb{VA}\).

International audience; There are several three-valued logical systems that form a scattered landscape, even if all reasonable connectives in three-valued logics can be derived from a few of them. Most papers on this subject neglect the issue of the relevance of such logics in relation with the intended meaning of the third truth-value. Here, we focus on the case where the third truth-value means unknown, as suggested by Kleene. Under such an understanding, we show that any truth-qualified formula in a large range of three-valued logics can be translated into KD as a modal formula of depth 1, with modalities in front of literals only, while preserving all tautologies and inference rules of the original three-valued logic. This simple information logic is a two-tiered classical propositional logic with simple semantics in terms of epistemic states understood as subsets of classical interpretations. We study in particular the translations of Kleene, Gödel, ᴌukasiewicz and Nelson logics. We show that Priest’s logic of paradox, closely connected to Kleene’s, can also be translated into our modal setting, simply by exchanging the modalities possible and necessary. Our work enables the precise expressive power of three-valued logics to be laid bare for the purpose of uncertainty management.

International audience; The logic of Bunched implications (BI) and its variants or extensions provide a powerful framework to deal with resources having static properties. Inthis paper, we propose a modal extension of BI logic, called DBI, which allows us to deal with dynamic resource properties. After defining a Kripke semantics for DBI, we illustrate the interest of DBI for expressing some dynamic properties and then we propose a labelled tableaux calculus for this logic. This calculus is proved sound and complete w.r.t. the Kripke semantics. Moreover, we also give a method for counter-model generation in this logic.

The modal systems S1--S3 were introduced by C. I. Lewis as logics for strict implication. While there are Kripke semantics for S2 and S3, there is no known natural semantics for S1. We extend S1 by a Substitution Principle SP which generalizes a reference rule of S1. In system S1+SP, the relation of strict equivalence $\varphi\equiv\psi$ satisfies the identity axioms of R. Suszko's non-Fregean logic adapted to the language of modal logic (we call these axioms the axioms of propositional identity). This enables us to develop a framework of algebraic semantics which captures S1+SP as well as the Lewis systems S3--S5. So from the viewpoint of algebraic semantics, S1+SP turns out to be an interesting modal logic. We show that S1+SP is strictly contained between S1 and S3 and differs from S2. It is the weakest modal logic containing S1 such that strict equivalence is axiomatized by propositional identity., Comment: 14 pages, thoroughly revised and extended version, title has changed

This paper presents an algebraic approach of some many-valued generalizations of modal logic. The starting point is the definition of the [0, 1]-valued Kripke models, where [0, 1] denotes the well known MV-algebra. Two types of structures are used to define validity of formulas: the class of frames and the class of Łn-valued frames. The latter structures are frames in which we specify in each world u the set (a subalgebra of Łn) of the allowed truth values of the formulas in u. We apply and develop algebraic tools (namely, canonical and strong canonical extensions) to generate complete modal n + 1-valued logics and we obtain many-valued counterparts of Shalqvist canonicity result.

This is Part 1 of a paper on fibred semantics and combination of logics. It aims to present a methodology for combining arbitrary logical systemsLi,i∈I, to form a new systemLI. The methodology ‘fibres’ the semanticsiofLiinto a semantics forLI, and ‘weaves’ the proof theory (axiomatics) ofLiinto a proof system ofLI. There are various ways of doing this, we distinguish by different names such as ‘fibring’, ‘dovetailing’ etc, yielding different systems, denoted byetc. Once the logics are ‘weaved’, further ‘interaction’ axioms can be geometrically motivated and added, and then systematically studied. The methodology is general and is applied to modal and intuitionistic logics as well as to general algebraic logics. We obtain general results on bulk, in the sense that we develop standard combining techniques and refinements which can be applied to any family of initial logics to obtain further combined logics.The main results of this paper is a construction for combining arbitrary, (possibly not normal) modal or intermediate logics, each complete for a class of (not necessarily frame) Kripke models. We show transfer of recursive axiomatisability, decidability and finite model property.Some results on combining logics (normal modal extensions ofK) have recently been introduced by Kracht and Wolter, Goranko and Passy and by Fine and Schurz as well as a multitude of special combined systems existing in the literature of the past 20–30 years. We hope our methodology will help organise the field systematically.

We characterize the bimodal provability logics for certain natural (classes of) pairs of recursively enumerable theories, mostly related to fragments of arithmetic. For example, we shall give axiomatizations, decision procedures, and introduce natural Kripke semantics for the provability logics of (IΔ0 + EXP, PRA); (PRA, IΣn); (IΣm, IΣn) for 1 ≤ m < n; (PA, ACA0); (ZFC, ZFC + CH); (ZFC, ZFC + ¬CH) etc. For the case of finitely axiomatized extensions of theories these results are extended to modal logics with propositional constants.

Based on the results of [11] this paper delivers uniform algorithms for deciding whether a finitely axiomatizable tense logic has the finite model property, is complete with respect to Kripke semantics, is strongly complete with respect to Kripke semantics, is d-persistent, is r-persistent. It is also proved that a tense logic is strongly complete iff the corresponding variety of bimodal algebras is complex, and that a tense logic is d-persistent iff it is complete and its Kripke frames form a first order definable class. From this we obtain many natural non-d-persistent tense logics whose corresponding varieties of bimodal algebras are complex. Mathematics Subject Classification: 03B45, 03B25.

Modal logics are currently widely accepted as a suitable tool of knowledge representation, and the question what logics are better suited for representing knowledge is of particular importance. Usually, some axiom list is given, and arguments are presented justifying that suggested axioms agree with intuition. The question why the suggested axioms describe all the desired properties of knowledge remains answered only partially, by showing that the most obvious and popular additional axioms would violate the intuition. We suggest the general paradigm of maximal logics and demonstrate how it can work for nonmonotonic modal logics. Technically, we prove that each of the modal logics KD45, SW5, S4F and S4.2 is the strongest modal logic among the logics generating the same nonmonotonic logic. These logics have already found important applications in knowledge representation, and the obtained results contribute to the explanation of this fact.

We are accustomed to regardingKas the weakest modal logic admitting of a relational semantics in the style made popular by Kripke. However, in a series of papers which demonstrates a startling connection between modal logic and the theory of paraconsistent inference, Ray Jennings and Peter Schotch have developed a generalized relational frame theory which articulates an infinite hierarchy of sublogics ofK, each expressing a species of “weakly aggregative necessity”. Recall thatKis axiomatized, in the presence ofNandRM, by the schema of “binary aggregation”For eachn≥ 1, the weakly aggregative modal logicKnis axiomatized by replacingKwith the schema of “n-ary aggregation”which is ann-ary relaxation, or weakening, ofK. Note thatK1=K.In [3], the authors claim without proof thatKnis determined by the class of framesF= (W, R), whereWis a nonempty set andRis an (n+ 1)-ary relation onW, under the generalization of Kriple's truth condition according to which □αis true at a pointwinWif and only ifαis true at one ofx1,…,xnfor allx1,…,xninWsuch thatRw, x1,…,xn.

We continue a series of papers on a family of many-valued modal logics, a family whose Kripke semantics involves many-valued accessibility relations. Earlier papers in the series presented a motivation in terms of a multiple-expert semantics. They also proved completeness of sequent calculus formulations for the logics, formulations using a cut rule in an essential way. In this paper a novel cut-free tableau formulation is presented, and its completeness is proved.

In this paper we develop a general framework to deal with abstract logics associated with a given modal logic. In particular we study the abstract logics associated with the weak and strong deductive systems of the normal modal logicK and its intuitionistic version. We also study the abstract logics that satisfy the conditionC +(X)=C(∪ i≤n I n X) and find the modal deductive systems whose abstract logics, in addition to being classical or intuitionistic, satisfy that condition. Finally we study the deductive systems whose abstract logics satisfy, in addition to the already mentioned properties, the property that the operatorC + is classical relative to some new defined operations.

We prove that a natural and simple predicate modal logic with the Barcan formula, namely QBF-KD plus the axiom of density, is not Kripke complete. Although incompleteness results are known in Kripke semantics, most of the methods used can only apply to logics stronger than QBF-S4 as they are based in a translation from intermediate logics. We give here an original proof of this incompleteness result.

We study modal logics based on neighbourhood semantics using methods and theorems having their origin in topological model theory. We thus obtain general results concerning completeness of modal logics based on neighbourhood semantics as well as the relationship between neighbourhood and Kripke semantics. We also give a new proof for a known interpolation result of modal logic using an interpolation theorem of topological model theory.

The paper presents aset-theoretic translation method for polymodal logics that reduces derivability in a large class of propositional polymodal logics to derivability in a very weak first-order set theory Ω. Unlike most existing translation methods, the one we propose applies to any normal complete finitely axiomatizable polymodal logic, regardless of whether it is first-order complete or an explicit semantics is available. The finite axiomatizability of Ω allows one to implement mechanical proof-search procedures via the deduction theorem. Alternatively, more specialized and efficient techniques can be employed. In the last part of the paper, we briefly discuss the application ofset T-resolution to support automated derivability in (a suitable extension of) Ω.

We give an overview of decidability results for modal logics having a binary modality. We put an emphasis on the demonstration of proof-techniques, and hope that this will also help in finding the borderlines between decidable and undecidable fragments of usual first-order logic.

In this paper, the modal logic over classes of structures definable by universal first-order Horn formulas is studied. We show that the satisfiability problems for that logics are decidable, confirming the conjecture from [E. Hemaspaandra and H. Schnoor, On the Complexity of Elementary Modal Logics, STACS 08]. We provide a full classification of logics defined by universal first-order Horn formulas, with respect to the complexity of satisfiability of modal logic over the classes of frames they define. It appears, that except for the trivial case of inconsistent formulas for which the problem is in P, local satisfiability is either NP-complete or PSPACE-complete, and global satisfiability is NP-complete, PSPACE-complete, or EXPTIME-complete. While our results holds even if we allow to use equality, we show that inequality leads to undecidability.

In this work, we combine the frameworks of Justification Logics and Logics of Plausibility-Based Beliefs to build a logic for Multi-Agent Systems where each agent can explicitly state his justification for believing in a given sentence. Our logic is a normal modal logic based on the standard Kripke semantics, where we provide a semantic definition for the evidence terms and define the notion of plausible evidence for an agent, based on plausibility relations in the model. This way, unlike traditional Justification Logics, justifications can be actually faulty and unreliable. In our logic, agents can disagree not only over whether a sentence is true or false, but also on whether some evidence is a valid justification for a sentence or not. After defining our logic and its semantics, we provide a strongly complete axiomatic system for it and show that it has the finite model property and is decidable. Thus, this logic seems to be a good first step for the development of a dynamic logic that can model the processes of argumentation and debate in multi-agent systems.

Morphological operators are generalized to lattices as adjunction pairs (Serra, 1984; Ronse, 1990; Heijmans and Ronse, 1990; Heijmans, 1994). In particular, morphology for set lattices is applied to analyze logics through Kripke semantics (Bloch, 2002; Fujio and Bloch, 2004; Fujio, 2006). For example, a pair of morphological operators as an adjunction gives rise to a temporalization of normal modal logic (Fujio and Bloch, 2004; Fujio, 2006). Also, constructions of models for intuitionistic logic or linear logics can be described in terms of morphological interior and/or closure operators (Fujio and Bloch, 2004). This shows that morphological analysis can be applied to various non-classical logics. On the other hand, quantum logics are algebraically formalized as orhomodular or modular ortho-complemented lattices (Birkhoff and von Neumann, 1936; Maeda, 1980; Chiara and Giuntini, 2002), and shown to allow Kripke semantics (Chiara and Giuntini, 2002). This suggests the possibility of morphological analysis for quantum logics. In this article, to show an efficiency of morphological analysis for quantum logic, we consider the implication problem in quantum logics (Chiara and Giuntini, 2002). We will give a comparison of the 5 polynomial implication connectives available in quantum logics.

We present a semantic study of a family of modal intuitionistic linear systems, providing various logics with both an algebraic semantics and a relational semantics, to obtain completeness results. We call modality a unary operator □ on formulas which satisfies only one rale (regularity), and we consider any subsetW of a list of axioms which defines the exponential “of course” of linear logic. We define an algebraic semantics by interpreting the modality □ as a unary operationμ on an IL-algebra. Then we introduce a relational semantics based on pretopologies with an additional binary relationr between information states. The interpretation of □ is defined in a suitable way, which differs from the traditional one in classical modal logic. We prove that such models provide a complete semantics for our minimal modal system, as well as, by requiring the suitable conditions onr (in the spirit of correspondence theory), for any of its extensions axiomatized by any subsetW as above. We also prove an embedding theorem for modal IL-algebras into complete ones and, after introducing the notion of general frame, we apply it to obtain a duality between general frames and modal IL-algebras.

We present tableau systems and sequent calculi for the intuitionistic analoguesIK, ID, IT, IKB, IKDB, IB, IK4, IKD4, IS4, IKB4, IK5, IKD5, IK45, IKD45 andIS5 of the normal classical modal logics. We provide soundness and completeness theorems with respect to the models of intuitionistic logic enriched by a modal accessibility relation, as proposed by G. Fischer Servi. We then show the disjunction property forIK, ID, IT, IKB, IKDB, IB, IK4, IKD4, IS4, IKB4, IK5, IK45 andIS5. We also investigate the relationship of these logics with some other intuitionistic modal logics proposed in the literature.

The main result of this paper is the following theorem: each modal logic extendingK4 having the branching property belowm and the effective m-drop point property is decidable with respect to admissibility. A similar result is obtained for intermediate intuitionistic logics with the branching property belowm and the strong effective m-drop point property. Thus, general algorithmic criteria which allow to recognize the admissibility of inference rules for modal and intermediate logics of the above kind are found. These criteria are applicable to most modal logics for which decidability with respect to admissibility is known and to many others, for instance, to the modal logicsK4,K4.1,K4.2,K4.3,S4.1,S4.2,GL.2; to all smallest and greatest counterparts of intermediate Gabbay-De-Jong logicsDn; to all intermediate Gabbay-De-Jong logicsDn; to all finitely axiomatizable modal and intermediate logics of finite depth etc. Semantic criteria for recognizing admissibility for these logics are offered as well.

This paper presents a logic for reasoning about information change in multi-agent settings based on epistemic arrow deletion in Kripke models.

This article deals with many-valued modal logics, based only on the necessity operator, over a residuated lattice. We focus on three basic classes, according to the accessibility relation, of Kripke frames: the full class of frames evaluated in the residuated lattice (and so defining the minimum modal logic), the ones evaluated in the idempotent elements and the ones only evaluated in 0 and 1. We show how to expand an axiomatization, with canonical truth-constants in the language, of a finite residuated lattice into one of the modal logic, for each one of the three basic classes of Kripke frames. We also provide axiomatizations for the case of a finite MV chain but this time without canonical truth-constants in the language. © 2009 The Author., The collaborative work between the authors of this article was made possible by several research grants: CyT-UBA X484, research CONICET program PIP 5541, AT Consolider CSD2007-0022 LOMOREVI Eurocores Project FP006/FFI2008-03126-E/FILO, MULOG2 TIN2007-68005-C04-01 of the Spanish Ministry of Education and Science, including feder funds of the European Union, and 2009SGR-1433/1434 of the Catalan Government

Dynamic modal logics are modal logics that have statements of the form [?]?. The truth value of such statements, when evaluated in a pointed model (M, w), is determined by the truth value that ? takes in some or all of the pointed models (M , w) that stand in a relation ??? to (M, w). This paper introduces new dynamic operators that minimally revise finite classical Kripke models to make almost any satisfiable modal formula ? true. To this end, we define two minimal revision relations ?+?? and ?++??. The first revises only the valuation function whereas the second relation also changes the frame. Our approach is different from others in that (i) our revision expressions ? do not refer to abstract semantic objects such as accessibility relations or 'action models', (ii) we do not add extra semantic structure to our models, and (iii) yet we can make almost any formula true.

In this paper, we give a logic for perception and knowledge: Flatland. This semantics of this framework is a concrete Kripke model so that it is an easy-to-understand toy example for students. We present a piece of software called Plaza's world enabling to check formulas in such a concrete Kripke model and to announce formulas.

Modal logics are widely used in computer science. The complexity of their satisfiability problems has been an active field of research since the 1970s. We prove that even very "simple" modal logics can be undecidable: We show that there is an undecidable unimodal logic that can be obtained by restricting the allowed models with an equality-free first-order formula in which only universal quantifiers appear.

We consider the Boolean modal logic wK4Dyn for which we prove topological and Kripke completeness results. The main result is to show that wK4Dyn is expressively equivalent to the extended language with common belief and distributed belief operators over the class of all weakly transitive, regular Kripke frames.

Many nonmonotonic formalism, including default logic, logic programming with stable models, and autoepistemic logic, can be represented faithfully by means of modal nonmonotonic logics in the family proposed by McDermott and Doyle. In this paper properties of logics in this family are thoroughly investigated. We present several results on characterization of expansions. These results are applicable to a wide class of nonmonotonic modal logics. Using these characterization results, algorithms for computing expansions for finite theories are developed. Perhaps the most important finding of this paper is that the structure of the family of modal nonmonotonic logics is much simpler than that of the family of underlying modal (monotonic) logics. Namely, it is often the case that different monotonic modal logics collapse to the same nonmonotonic system. We exhibit four families of logics whose nonmonotonic variants coincide: 5-KD45, TW5-SW5, N-WK , and W5-D4WB . These nonmonotonic logics naturally represent logics related to commonsense reasoning and knowledge representation such as autoepistemic logic, reflexive autoepistemic logic, default logic, and truth maintenance with negation.

Whether possible worlds are understood realistically, actualistically, or heuristically, it is interesting that a large and natural class of modal logics can be characterized by means of a semantics in which possibility and necessity are interpreted as quantifiers over possible worlds. The quantificational interpretation of l and O is interesting not only because it marks off a natural and applicable class of modal logics from the rest, but also because it illuminates the logics it marks off in two ways: since, in each case, O is interpreted as a universal quantifier over alternative possible worlds, we have an account of what is the same about the meaning of Ol from one system of modal logic to the next. And since the properties of the alternativeness relation vary among different modal systems, we also have an account of how the meaning of O differs from one system to the next. In this paper I will develop a probabilistic semantics for modal logic that preserves this quantificational apparatus, with its vocabulary for saying what is the same and what is different about the meaning of necessity in different modal logics. My aim is to develop a species of generalized Kripke model for modal logic, based on the idea that Popper functions are a kind of generalized truth valuation. This aim is consistent with the central motivation of probabilistic semantics: to interpret systems of logic without appealing to reference or truth conditions.' Nevertheless, the aim of this paper is clearly at odds with the views of others who have worked on probabilistic semantics for modal logic. In [12] Charles Morgan presents a quantification-based probabilistic semantics for modal logic but makes it clear in [10], where he presents a non-quantification-based probabilistic semantics for modal logic, that he regards the quantificational approach as such as being philosophically inferior. Needless to say, I disagree with Morgan's philosophical assessment of the quantificational approach. In my view, once the ontologically problematic

The LogicR4 is obtained by adding the axiom ▭(A vB→(◊Av▭B) to the modal relevant logicNR. We produce a model theory for this logic and show completeness. We also show that there is a natural embedding of a Kripke model forS4 in eachR4 model structure.

Some properties of Kripke-sheaf semantics for super-intuitionistic predicate logics are shown. The concept ofp-morphisms between Kripke sheaves is introduced. It is shown that if there exists ap-morphism from a Kripke sheaf κ1 into κ2 then the logic characterized by κ1 is contained in the logic characterized by κ2. Examples of Kripke-sheaf complete and finitely axiomatizable super-intuitionistic (and intermediate) predicate logics each of which is Kripke-frame incomplete are given. A correction to the author's previous paper “Kripke bundles for intermediate predicate logics and Kripke frames for intuitionistic modal logics” (Studia Logica, 49(1990), pp. 289–306 ) is stated.

We present sequent calculi for normal modal logics where modal and propositional behaviours are separated, and we prove a cut elimination theorem for the basic system K, so as completeness theorems (in the new style) both for K itself and for its most popular enrichments. MSC: 03B45, 03F05.

In this paper I give conditions under which a matrix characterisation of validity is correct for first order logics where quantifications are restricted by statements from a theory. Unfortunately the usual definition of path closure in a matrix is unsuitable and a less pleasant definition must be used. I derive the matrix theorem from syntactic analysis of a suitable tableau system, but by choosing a tableau system for restricted quantification I generalise Wallen's earlier work on modal logics. The tableau system is only correct if a new condition I call “alphabetical monotonicity” holds. I sketch how the result can be applied to a wide range of logics such as first order variants of many standard modal logics, including non-serial modal logics.

In a narrow sense, modal logic is a logic obtained from the classical logic by endowing it with unary propositional operations intuitively corresponding to ‘it is necessary that’ and ‘it is possible that’. These operations are intensional, i.e., the truth of a formula built with the operation does not depend only on the truth of the subformula to which the operation is applied but also on a relevant state or a situation in which the truth is considered. A development of the semantics of modal logics in terms of a relational structure of states is due to Stig Kanger [Kan57] and Saul Kripke [Kri63]. Algebraic semantics of these standard modal logics is provided by Boolean algebras with normal and additive operations [JT52]. Since the origin of Kripke semantics, intensional logics have been introduced to computer science as an important tool for its formal methods.

International audience; In this paper we study natural deduction for the intuitionistic and classical (normal) modal logics obtained from the combinations of the axioms T, B, 4 and 5. In this context we introduce a new multi-contextual structure, called T-sequent, that allows to design simple labelfree natural deduction systems for these logics. After proving that they are sound and complete we show that they satisfy the normalization property and consequently the subformula property in the intuitionistic case.

Deciding whether a modal formula is satisfiable with respect to a given set of (global) assumptions is a question of fundamental importance in applications of logic in computer science. Tableau methods have proved extremely versatile for solving this problem for many different individual logics but they typically do not meet the known complexity bounds for the logics in question. Recently, it has been shown that optimality can be obtained for some logics while retaining practicality by using a technique called "global caching". Here, we show that global caching is applicable to all logics that can be equipped with coalgebraic semantics, for example, classical modal logic, graded modal logic, probabilistic modal logic and coalition logic. In particular, the coalgebraic approach also covers logics that combine these various features. We thus show that global caching is a widely applicable technique and also provide foundations for optimal tableau algorithms that uniformly apply to a large class of modal logics. © 2010 Springer-Verlag.

We study the model checking problem for logics whose semantics are defined using transitive Kripke models. We show that the model checking problem is P-complete for the intuitionistic logic KC. Interestingly, for its modal companion S4.2 we also obtain P-completeness even if we consider formulas with one variable only. This result is optimal since model checking for S4 without variables is NC1-complete. The strongest variable free modal logic with P-complete model checking problem is K4. On the other hand, for KC formulas with one variable only we obtain much lower complexity, namely LOGDCFL as an upper bound.

In this Chapter we focus on the class of non-axiomatic systems that are called standard in the sense of keeping intact all the machinery of suitable systems for classical logic. Extensions are obtained by means of additional modal rules. This group covers modal extensions of standard Gentzen SC, Hintikka-style modal TS, and some ND systems.