-
50Logic in computer science: Modelling and reasoning about systems (review)Journal of Logic, Language and Information 16 (1): 117-120. 2006.Book review
-
24Foreword to Special issue on Logics for Multi-agent SystemsJournal of Applied Non-Classical Logics 21 (1): 7-8. 2011.Foreword to Special issue on Logics for Multi-agent Systems
-
220Tableaux-based decision method for single-agent linear time synchronous temporal epistemic logics with interacting time and knowledgeIn Kamal Lodaya (ed.), Logic and Its Applications, Springer. pp. 80--96. 2013.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
-
446Elementary canonical formulae: extending Sahlqvist’s theoremAnnals 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
-
209Proving unprovability in some normal modal logicsBulletin of the Section of Logic 20 (1): 23-29. 1991.This note considers deductive systems for the operator a of unprovability in some particular propositional normal modal logics. We give thus complete syntactic characterization of these logics in the sense of Lukasiewicz: for every formula either ` or a (but not both) is derivable. In particular, purely syntactic decision procedure is provided for the logics under considerations.
-
31Modal logic, Alexander Chagrov and Michael Zakharyaschev (review)Journal of Logic, Language and Information 8 (2): 255-258. 1999.Book review
-
352Propositional interval neighborhood logics: Expressiveness, decidability, and undecidable extensionsAnnals 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
-
364Modal Logics for Parallelism, Orthogonality, and Affine GeometriesJournal 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.
-
211Algorithmic correspondence and completeness in modal logic. IV. Semantic extensions of SQEMAJournal 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
-
670A Road Map of Interval Temporal Logics and Duration CalculiJournal 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.
-
327The modal logic of the countable random frameArchive 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
-
326Logic for physical space: From antiquity to present daysSynthese 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
-
392Temporal Logics with Reference Pointers and Computation Tree LogicsJournal 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
-
321Hyperboolean Algebras and Hyperboolean Modal LogicJournal 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
-
623The Craig interpolation theorem for prepositional logics with strong negationStudia Logica 44 (3). 1985.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.
-
310Model-checking CTL* over flat Presburger counter systemsJournal 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
-
318Modal definability in enriched languagesNotre 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
-
444Refutation systems in modal logicStudia 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.
-
628Modal logic with namesJournal 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
-
361Hierarchies of modal and temporal logics with reference pointersJournal 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
-
493Axiomatizations with context rules of inference in modal logicStudia 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.
-
129Comparing semantics of logics for multi-agent systemsSynthese 139 (2). 2004.We draw parallels between several closely related logics that combine — in different proportions — elements of game theory, computation tree logics, and epistemic logics to reason about agents and their abilities. These are: the coalition game logics CL and ECL introduced by Pauly 2000, the alternating-time temporal logic ATL developed by Alur, Henzinger and Kupferman between 1997 and 2002, and the alternating-time temporal epistemic logic ATEL by van der Hoek and Wooldridge (2002). In particula…Read more
-
71An extended branching-time ockhamist temporal logicJournal of Logic, Language and Information 8 (2): 143-166. 1999.For branching-time temporal logic based on an Ockhamist semantics, we explore a temporal language extended with two additional syntactic tools. For reference to the set of all possible futures at a moment of time we use syntactically designated restricted variables called fan-names. For reference to all possible futures alternative to the actual one we use a modification of a difference modality, localized to the set of all possible futures at the actual moment of time.We construct an axiomatic …Read more
Areas of Specialization
Science, Logic, and Mathematics |
Areas of Interest
Science, Logic, and Mathematics |