•  594
    A Road Map of Interval Temporal Logics and Duration Calculi
    with Angelo Montanari and Guido Sciavicco
    Journal of Applied Non-Classical Logics 14 (1-2): 9-54. 2004.
    We survey main developments, results, and open problems on interval temporal logics and duration calculi. We present various formal systems studied in the literature and discuss their distinctive features, emphasizing on expressiveness, axiomatic systems, and (un)decidability results.
  •  542
    This paper deals with, prepositional calculi with strong negation (N-logics) in which the Craig interpolation theorem holds. N-logics are defined to be axiomatic strengthenings of the intuitionistic calculus enriched with a unary connective called strong negation. There exists continuum of N-logics, but the Craig interpolation theorem holds only in 14 of them.
  •  512
    From Linear to Branching-Time Temporal Logics: Transfer of Semantics and Definability
    with Alberto Zanardo
    Logic Journal of the IGPL 15 (1): 53-76. 2007.
    This paper investigates logical aspects of combining linear orders as semantics for modal and temporal logics, with modalities for possible paths, resulting in a variety of branching time logics over classes of trees. Here we adopt a unified approach to the Priorean, Peircean and Ockhamist semantics for branching time logics, by considering them all as fragments of the latter, obtained as combinations, in various degrees, of languages and semantics for linear time with a modality for possible pa…Read more
  •  500
    Modal logic with names
    with George Gargov
    Journal of Philosophical Logic 22 (6). 1993.
    We investigate an enrichment of the propositional modal language L with a "universal" modality ■ having semantics x ⊧ ■φ iff ∀y(y ⊧ φ), and a countable set of "names" - a special kind of propositional variables ranging over singleton sets of worlds. The obtained language ℒ $_{c}$ proves to have a great expressive power. It is equivalent with respect to modal definability to another enrichment ℒ(⍯) of ℒ, where ⍯ is an additional modality with the semantics x ⊧ ⍯φ iff Vy(y ≠ x → y ⊧ φ). Model-theo…Read more
  •  461
    Classes and theories of trees associated with a class of linear orders
    with Ruaan Kellerman
    Logic Journal of the IGPL 19 (1): 217-232. 2011.
    Given a class of linear order types C, we identify and study several different classes of trees, naturally associated with C in terms of how the paths in those trees are related to the order types belonging to C. We investigate and completely determine the set-theoretic relationships between these classes of trees and between their corresponding first-order theories. We then obtain some general results about the axiomatization of the first-order theories of some of these classes of trees in term…Read more
  •  427
    Axiomatizations with context rules of inference in modal logic
    Studia Logica 61 (2): 179-197. 1998.
    A certain type of inference rules in modal logics, generalizing Gabbay's Irreflexivity rule, is introduced and some general completeness results about modal logics axiomatized with such rules are proved.
  •  363
    Elementary canonical formulae: extending Sahlqvist’s theorem
    Annals of Pure and Applied Logic 141 (1): 180-217. 2006.
    We generalize and extend the class of Sahlqvist formulae in arbitrary polyadic modal languages, to the class of so called inductive formulae. To introduce them we use a representation of modal polyadic languages in a combinatorial style and thus, in particular, develop what we believe to be a better syntactic approach to elementary canonical formulae altogether. By generalizing the method of minimal valuations à la Sahlqvist–van Benthem and the topological approach of Sambin and Vaccaro we prove…Read more
  •  352
    Refutation systems in modal logic
    Studia Logica 53 (2). 1994.
    Complete deductive systems are constructed for the non-valid (refutable) formulae and sequents of some propositional modal logics. Thus, complete syntactic characterizations in the sense of Lukasiewicz are established for these logics and, in particular, purely syntactic decision procedures for them are obtained. The paper also contains some historical remarks and a general discussion on refutation systems.
  •  338
    Temporal Logics with Reference Pointers and Computation Tree Logics
    Journal of Applied Non-Classical Logics 10 (3): 221-242. 2000.
    A complete axiomatic system CTL$_{rp}$ is introduced for a temporal logic for finitely branching $\omega^+$-trees in a temporal language extended with so called reference pointers. Syntactic and semantic interpretations are constructed for the branching time computation tree logic CTL$^{*}$ into CTL$_{rp}$. In particular, that yields a complete axiomatization for the translations of all valid CTL$^{*}$-formulae. Thus, the temporal logic with reference pointers is brought forward as a simpler …Read more
  •  327
    We develop a conceptually clear, intuitive, and feasible decision procedure for testing satisfiability in the full multi\-agent epistemic logic \CMAELCD\ with operators for common and distributed knowledge for all coalitions of agents mentioned in the language. To that end, we introduce Hintikka structures for \CMAELCD\ and prove that satisfiability in such structures is equivalent to satisfiability in standard models. Using that result, we design an incremental tableau-building procedure that e…Read more
  •  318
    Sahlqvist Formulas Unleashed in Polyadic Modal Languages
    In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic, Csli Publications. pp. 221-240. 1998.
    We propose a generalization of Sahlqvist formulae to polyadic modal languages by representing modal polyadic languages in a combinatorial style and thus, in particular, developing what we believe to be the right approach to Sahlqvist formulae at all. The class of polyadic Sahlqvist formulae PSF defined here expands essentially the so far known one. We prove first-order definability and canonicity for the class PSF.
  •  300
    Sahlqvist Formulas Unleashed in Polyadic Modal Languages
    In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic, Csli Publications. pp. 221-240. 1998.
    We propose a generalization of Sahlqvist formulas to polyadic modal languages by representing such languages in a combinatorial PDL style and thus, in particular, developing what we believe to be the right syntactic approach to Sahlqvist formulas at all. The class of polyadic Sahlqvist formulas PSF defined here expands essentially the so far known one. We prove first-order definability and canonicity for the class PSF.
  •  297
    Modal Logics for Parallelism, Orthogonality, and Affine Geometries
    with Philippe Balbiani
    Journal of Applied Non-Classical Logics 12 (3-4): 365-397. 2002.
    We introduce and study a variety of modal logics of parallelism, orthogonality, and affine geometries, for which we establish several completeness, decidability and complexity results and state a number of related open, and apparently difficult problems. We also demonstrate that lack of the finite model property of modal logics for sufficiently rich affine or projective geometries (incl. the real affine and projective planes) is a rather common phenomenon.
  •  295
    Hierarchies of modal and temporal logics with reference pointers
    Journal of Logic, Language and Information 5 (1): 1-24. 1996.
    We introduce and study hierarchies of extensions of the propositional modal and temporal languages with pairs of new syntactic devices: point of reference-reference pointer which enable semantic references to be made within a formula. We propose three different but equivalent semantics for the extended languages, discuss and compare their expressiveness. The languages with reference pointers are shown to have great expressive power (especially when their frugal syntax is taken into account), per…Read more
  •  294
    Logic for physical space: From antiquity to present days
    with Marco Aiello, Guram Bezhanishvili, and Isabelle Bloch
    Synthese 186 (3): 619-632. 2012.
    Since the early days of physics, space has called for means to represent, experiment, and reason about it. Apart from physicists, the concept of space has intrigued also philosophers, mathematicians and, more recently, computer scientists. This longstanding interest has left us with a plethora of mathematical tools developed to represent and work with space. Here we take a special look at this evolution by considering the perspective of Logic. From the initial axiomatic efforts of Euclid, we rev…Read more
  •  293
    Propositional interval neighborhood logics: Expressiveness, decidability, and undecidable extensions
    with Davide Bresolin, Angelo Montanari, and Guido Sciavicco
    Annals of Pure and Applied Logic 161 (3): 289-304. 2010.
    In this paper, we investigate the expressiveness of the variety of propositional interval neighborhood logics , we establish their decidability on linearly ordered domains and some important subclasses, and we prove the undecidability of a number of extensions of PNL with additional modalities over interval relations. All together, we show that PNL form a quite expressive and nearly maximal decidable fragment of Halpern–Shoham’s interval logic HS
  •  293
    The Basic Algebra of Game Equivalences
    Studia Logica 75 (2): 221-238. 2003.
    We give a complete axiomatization of the identities of the basic game algebra valid with respect to the abstract game board semantics. We also show that the additional conditions of termination and determinacy of game boards do not introduce new valid identities.En route we introduce a simple translation of game terms into plain modal logic and thus translate, while preserving validity both ways, game identities into modal formulae.The completeness proof is based on reduction of game terms to a …Read more
  •  289
    Algorithmic correspondence and completeness in modal logic. V. Recursive extensions of SQEMA
    with Willem Conradie and Dimitar Vakarelov
    Journal of Applied Logic 8 (4): 319-333. 2010.
    The previously introduced algorithm \sqema\ computes first-order frame equivalents for modal formulae and also proves their canonicity. Here we extend \sqema\ with an additional rule based on a recursive version of Ackermann's lemma, which enables the algorithm to compute local frame equivalents of modal formulae in the extension of first-order logic with monadic least fixed-points \mffo. This computation operates by transforming input formulae into locally frame equivalent ones in the pure frag…Read more
  •  281
    A general tableau method for propositional interval temporal logics: Theory and implementation
    with A. Montanari, P. Sala, and G. Sciavicco
    Journal of Applied Logic 4 (3): 305-330. 2006.
    In this paper we focus our attention on tableau methods for propositional interval temporal logics. These logics provide a natural framework for representing and reasoning about temporal properties in several areas of computer science. However, while various tableau methods have been developed for linear and branching time point-based temporal logics, not much work has been done on tableau methods for interval-based ones. We develop a general tableau method for Venema's \cdt\ logic interpreted o…Read more
  •  275
    The modal logic of the countable random frame
    with Bruce Kapron
    Archive for Mathematical Logic 42 (3): 221-243. 2003.
    We study the modal logic M L r of the countable random frame, which is contained in and `approximates' the modal logic of almost sure frame validity, i.e. the logic of those modal principles which are valid with asymptotic probability 1 in a randomly chosen finite frame. We give a sound and complete axiomatization of M L r and show that it is not finitely axiomatizable. Then we describe the finite frames of that logic and show that it has the finite frame property and its satisfiability problem …Read more
  •  265
    Hyperboolean Algebras and Hyperboolean Modal Logic
    Journal of Applied Non-Classical Logics 9 (2): 345-368. 1999.
    Hyperboolean algebras are Boolean algebras with operators, constructed as algebras of complexes (or, power structures) of Boolean algebras. They provide an algebraic semantics for a modal logic (called here a {\em hyperboolean modal logic}) with a Kripke semantics accordingly based on frames in which the worlds are elements of Boolean algebras and the relations correspond to the Boolean operations. We introduce the hyperboolean modal logic, give a complete axiomatization of it, and show that i…Read more
  •  264
    Modal definability in enriched languages
    Notre Dame Journal of Formal Logic 31 (1): 81-105. 1989.
    The paper deals with polymodal languages combined with standard semantics defined by means of some conditions on the frames. So, a notion of "polymodal base" arises which provides various enrichments of the classical modal language. One of these enrichments, viz. the base £(R,-R), with modalities over a relation and over its complement, is the paper's main paradigm. The modal definability (in the spirit of van Benthem's correspondence theory) of arbitrary and ~-elementary classes of frames in th…Read more
  •  260
    Model-checking CTL* over flat Presburger counter systems
    with Stéphane Demri, Alain Finkel, and Govert van Drimmelen
    Journal of Applied Non-Classical Logics 20 (4): 313-344. 2010.
    This paper concerns model-checking of fragments and extensions of CTL* on infinite-state Presburger counter systems, where the states are vectors of integers and the transitions are determined by means of relations definable within Presburger arithmetic. In general, reachability properties of counter systems are undecidable, but we have identified a natural class of admissible counter systems (ACS) for which we show that the quantification over paths in CTL* can be simulated by quantification o…Read more
  •  243
    Strategic commitment and release in logics for multi-agent systems
    with Thomas Ågotnes and Wojciech Jamroga
    In this paper we analyze how the semantics of the Alternating-time Temporal Logic ATL$^*$ deals with agents' commitments to strategies in the process of formula evaluation. In (\acro{atl}$^*$), one can express statements about the strategic ability of an agent (or a coalition of agents) to achieve a goal $\phi$ such as: ``agent $i$ can choose a strategy such that, if $i$ follows this strategy then, no matter what other agents do, $\phi$ will always be true''. However, strategies in \a…Read more
  •  215
    Temporal Logics with Reference Pointers and Computation Tree Logics
    Journal of Applied Non-Classical Logics 10 (3-4): 221-242. 2000.
    ABSTRACT A complete axiomatic system CTLrp is introduced for a temporal logic for finitely branching ω+ -trees in a language extended with so called reference pointers. Syntactic and semantic interpretations are constructed for the branching time computation tree logic CTL* into CTLrp. In particular, that yields a complete axiomatization for the translations of all valid CTL*-formulae. Thus, the temporal logic with reference pointers is brought forward as a simpler (with no path quantifiers), bu…Read more
  •  197
    Optimal Decision Procedures for Satisfiability in Fragments of Alternating-time Temporal Logics
    with Steen Vester
    In Rajeev Goré, Barteld Kooi & Agi Kurucz (eds.), Advances in Modal Logic, Volume 10, College Publications. pp. 234-253. 2014.
    We consider several natural fragments of the alternating-time temporal logics ATL* and ATL with restrictions on the nesting between temporal operators and strategic quantifiers. We develop optimal decision procedures for satisfiability in these fragments, showing that they have much lower complexities than the full languages. In particular, we prove that the satisfiability problem for state formulae in the full `strategically flat' fragment of ATL* is PSPACE-complete, whereas the satisfiability …Read more
  •  186
    Elementary Canonical Formulae: A Survey on Syntactic, Algorithmic, and Modeltheoretic Aspects
    with W. Conradie and D. Vakarelov
    In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic, Csli Publications. pp. 17-51. 1998.
    In terms of validity in Kripke frames, a modal formula expresses a universal monadic second-order condition. Those modal formulae which are equivalent to first-order conditions are called elementary. Modal formulae which have a certain persistence property which implies their validity in all canonical frames of modal logics axiomatized with them, and therefore their completeness, are called canonical. This is a survey of a recent and ongoing study of the class of elementary and canonical modal f…Read more
  •  179
    Temporal epistemic logics are known, from results of Halpern and Vardi, to have a wide range of complexities of the satisfiability problem: from PSPACE, through non-elementary, to highly undecidable. These complexities depend on the choice of some key parameters specifying, inter alia, possible interactions between time and knowledge, such as synchrony and agents' abilities for learning and recall. In this work we develop practically implementable tableau-based decision procedures for deciding s…Read more
  •  176
    Modal Logic and Universal Algebra I: Modal Axiomatizations of Structures
    In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic, Csli Publications. pp. 265-292. 1998.
    We study the general problem of axiomatizing structures in the framework of modal logic and present a uniform method for complete axiomatization of the modal logics determined by a large family of classes of structures of any signature.
  •  174
    Algorithmic correspondence and completeness in modal logic. IV. Semantic extensions of SQEMA
    with Willem Conradie
    Journal of Applied Non-Classical Logics 18 (2): 175-211. 2008.
    In a previous work we introduced the algorithm \SQEMA\ for computing first-order equivalents and proving canonicity of modal formulae, and thus established a very general correspondence and canonical completeness result. \SQEMA\ is based on transformation rules, the most important of which employs a modal version of a result by Ackermann that enables elimination of an existentially quantified predicate variable in a formula, provided a certain negative polarity condition on that variable is sati…Read more