Order:
Disambiguations
Stéphane Demri [22]S. Demri [2]Stéphane P. Demri [1]
  1. Incomplete Information: Structure, Inference, Complexity.Stéphane P. Demri & Ewa S. Orłowska - 2006 - Studia Logica 84 (3):469-475.
  2.  16
    Deciding Regular Grammar Logics with Converse Through First-Order Logic.Stéphane Demri & Hans De Nivelle - 2005 - Journal of Logic, Language and Information 14 (3):289-329.
    We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  3. Reasoning About Sequences of Memory States.Rémi Brochenin, Stéphane Demri & Etienne Lozes - 2009 - Annals of Pure and Applied Logic 161 (3):305-323.
    Motivated by the verification of programs with pointer variables, we introduce a temporal logic whose underlying assertion language is the quantifier-free fragment of separation logic and the temporal logic on the top of it is the standard linear-time temporal logic LTL. We analyze the complexity of various model-checking and satisfiability problems for , considering various fragments of separation logic , various classes of models , and the influence of fixing the initial memory state. We provide a complete picture based on (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  4.  32
    A Completeness Proof for a Logic with an Alternative Necessity Operator.Stéphane Demri - 1997 - Studia Logica 58 (1):99-112.
    We show the completeness of a Hilbert-style system LK defined by M. Valiev involving the knowledge operator K dedicated to the reasoning with incomplete information. The completeness proof uses a variant of Makinson's canonical model construction. Furthermore we prove that the theoremhood problem for LK is co-NP-complete, using techniques similar to those used to prove that the satisfiability problem for propositional S5 is NP-complete.
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   2 citations  
  5.  36
    Model-Checking CTL* Over Flat Presburger Counter Systems.Stéphane Demri, Alain Finkel, Valentin Goranko & Govert van Drimmelen - 2010 - Journal of Applied Non-Classical Logics 20 (4):313-344.
    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 over tuples of natural numbers, eventually allowing translation of (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  6.  15
    Index of Authors of Volume 8.B. Aldag, G. Antoniou, T. Aoto, P. Blackburn, K. Britz, M. Brown, A. Bundy, R. Cox, M. De Rijke & S. Demri - 1999 - Journal of Logic, Language, and Information 8 (485):485.
  7.  5
    Uniform and Non Uniform Strategies for Tableaux Calculi for Modal Logics.Stéphane Demri - 1995 - Journal of Applied Non-Classical Logics 5 (1):77-96.
  8.  13
    Linear-Time Temporal Logics with Presburger Constraints: An Overview ★.Stéphane Demri - 2006 - Journal of Applied Non-Classical Logics 16 (3-4):311-347.
    We present an overview of linear-time temporal logics with Presburger constraints whose models are sequences of tuples of integers. Such formal specification languages are well-designed to specify and verify systems that can be modelled with counter systems. The paper recalls the general framework of LTL over concrete domains and presents the main decidability and complexity results related to fragments of Presburger LTL. Related formalisms are also briefly presented.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  9.  14
    Every Finitely Reducible Logic has the Finite Model Property with Respect to the Class of ♦-Formulae.Stéphane Demri & Ewa Orłowska - 1999 - Studia Logica 62 (2):177 - 200.
    In this paper a unified framework for dealing with a broad family of propositional multimodal logics is developed. The key tools for presentation of the logics are the notions of closure relation operation and monotonous relation operation. The two classes of logics: FiRe-logics (finitely reducible logics) and LaFiRe-logics (FiRe-logics with local agreement of accessibility relations) are introduced within the proposed framework. Further classes of logics can be handled indirectly by means of suitable translations. It is shown that the logics from (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  10.  11
    Extensions of Modal Logic S5 Preserving NP-Completeness.Stéphane Demri - 1997 - Bulletin of the Section of Logic 26 (2):73-84.
    Direct download  
     
    Export citation  
     
    My bibliography  
  11.  26
    On Modal Logics Characterized by Models with Relative Accessibility Relations: Part I.Stéphane Demri & Dov Gabbay - 2000 - Studia Logica 65 (3):323-353.
    This work is divided in two papers (Part I and Part II). In Part I, we study a class of polymodal logics (herein called the class of "Rare-logics") for which the set of terms indexing the modal operators are hierarchized in two levels: the set of Boolean terms and the set of terms built upon the set of Boolean terms. By investigating different algebraic properties satisfied by the models of the Rare-logics, reductions for decidability are established by faithfully translating the (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography  
  12.  12
    A Framework for the Transfer of Proofs, Lemmas and Strategies From Classical to Non Classical Logics.Ricardo Caferra, Stéphane Demri & Michel Herment - 1993 - Studia Logica 52 (2):197 - 232.
    There exist valuable methods for theorem proving in non classical logics based on translation from these logics into first-order classical logic (abbreviated henceforth FOL). The key notion in these approaches istranslation from aSource Logic (henceforth abbreviated SL) to aTarget Logic (henceforth abbreviated TL). These methods are concerned with the problem offinding a proof in TL by translating a formula in SL, but they do not address the very important problem ofpresenting proofs in SL via a backward translation. We propose a (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  13.  15
    A Logic with Relative Knowledge Operators.Stéphane Demri - 1999 - Journal of Logic, Language and Information 8 (2):167-185.
    We study a knowledge logic that assumes that to each set of agents, an indiscernibility relation is associated and the agents decide the membership of objects or states up to this indiscernibility relation. Its language contains a family of relative knowledge operators. We prove the decidability of the satisfiability problem, we show its EXPTIME-completeness and as a side-effect, we define a complete Hilbert-style axiomatization.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  14.  7
    Index of Authors of Volume 9.S. Aguzzoli, V. Akman, A. D. C. Bennett, P. Blackburn, S. Bringsjord, C. Caporale, A. Ciabattoni, B. J. Copeland, S. Demri & D. Dubois - 2000 - Journal of Logic, Language, and Information 9 (519):519.
    Direct download  
     
    Export citation  
     
    My bibliography  
  15.  6
    Separation Logics and Modalities: A Survey.Stéphane Demri & Morgan Deters - 2015 - Journal of Applied Non-Classical Logics 25 (1):50-99.
    Like modal logic, temporal logic, and description logic, separation logic has become a popular class of logical formalisms in computer science, conceived as assertion languages for Hoare-style proof systems with the goal to perform automatic program analysis. In a broad sense, separation logic is often understood as a programming language, an assertion language and a family of rules involving Hoare triples. In this survey, we present similarities between separation logic as an assertion language and modal and temporal logics. Moreover, we (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  16.  12
    On Modal Logics Characterized by Models with Relative Accessibility Relations: Part II.Stéphane Demri & Dov Gabbay - 2000 - Studia Logica 66 (3):349-384.
    This work is divided in two papers (Part I and Part II). In Part I, we introduced the class of Rare-logics for which the set of terms indexing the modal operators are hierarchized in two levels: the set of Boolean terms and the set of terms built upon the set of Boolean terms. By investigating different algebraic properties satisfied by the models of the Rare-logics, reductions for decidability were established by faithfully translating the Rare-logics into more standard modal logics (some (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography  
  17.  10
    Display Calculi for Logics with Relative Accessibility Relations.Stéphane Demri & Rajeev Goré - 2000 - Journal of Logic, Language and Information 9 (2):213-236.
    We define cut-free display calculi for knowledge logics wherean indiscernibility relation is associated to each set of agents, andwhere agents decide the membership of objects using thisindiscernibility relation. To do so, we first translate the knowledgelogics into polymodal logics axiomatised by primitive axioms and thenuse Kracht's results on properly displayable logics to define thedisplay calculi. Apart from these technical results, we argue thatDisplay Logic is a natural framework to define cut-free calculi for manyother logics with relative accessibility relations.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  18.  2
    Every Finitely Reducible Logic has the Finite Model Property with Respect to the Class of ♦-Formulae.Stéphane Demri & Ewa Orłowska - 1999 - Studia Logica 62 (2):177-200.
    In this paper a unified framework for dealing with a broad family of propositional multimodal logics is developed. The key tools for presentation of the logics are the notions of closure relation operation and monotonous relation operation. The two classes of logics: FiRe-logics and LaFiRe-logics are introduced within the proposed framework. Further classes of logics can be handled indirectly by means of suitable translations. It is shown that the logics from these classes have the finite model property with respect to (...)
    Direct download  
     
    Export citation  
     
    My bibliography  
  19. Complexity of Modal Logics with Presburger Constraints.Stéphane Demri & Denis Lugiez - 2010 - Journal of Applied Logic 8 (3):233-252.