1.  20
    Temporalising Tableaux.Roman Kontchakov, Carsten Lutz, Frank Wolter & Michael Zakharyaschev - 2004 - Studia Logica 76 (1):91 - 134.
    As a remedy for the bad computational behaviour of first-order temporal logic (FOTL), it has recently been proposed to restrict the application of temporal operators to formulas with at most one free variable thereby obtaining so-called monodic fragments of FOTL. In this paper, we are concerned with constructing tableau algorithms for monodic fragments based on decidable fragments of first-order logic like the two-variable fragment or the guarded fragment. We present a general framework that shows how existing decision procedures for first-order (...)
    Direct download (6 more)  
    Export citation  
    My bibliography   3 citations  
  2.  5
    PDL with Negation of Atomic Programs.Carsten Lutz & Dirk Walther - 2005 - Journal of Applied Non-Classical Logics 15 (2):189-213.
  3.  14
    2-ExpTime Lower Bounds for Propositional Dynamic Logics with Intersection.Martin Lange & Carsten Lutz - 2005 - Journal of Symbolic Logic 70 (4):1072-1086.
    In 1984, Danecki proved that satisfiability in IPDL, i.e., Propositional Dynamic Logic (PDL) extended with an intersection operator on programs, is decidable in deterministic double exponential time. Since then, the exact complexity of IPDL has remained an open problem: the best known lower bound was the ExpTime one stemming from plain PDL until, in 2004, the first author established ExpSpace-hardness. In this paper, we finally close the gap and prove that IPDL is hard for 2-ExpTime, thus 2-ExpTime-complete. We then sharpen (...)
    Direct download (4 more)  
    Export citation  
    My bibliography   1 citation  
  4.  30
    A Tableau Decision Algorithm for Modalized ALC with Constant Domains.Carsten Lutz, Holger Sturm, Frank Wolter & Michael Zakharyaschev - 2002 - Studia Logica 72 (2):199-232.
    The aim of this paper is to construct a tableau decision algorithm for the modal description logic K ALC with constant domains. More precisely, we present a tableau procedure that is capable of deciding, given an ALC-formula with extra modal operators (which are applied only to concepts and TBox axioms, but not to roles), whether is satisfiable in a model with constant domains and arbitrary accessibility relations. Tableau-based algorithms have been shown to be practical even for logics of rather high (...)
    Direct download (8 more)  
    Export citation  
    My bibliography  
  5.  14
    PDL with Intersection and Converse: Satisfiability and Infinite-State Model Checking.Stefan Göller, Markus Lohrey & Carsten Lutz - 2009 - Journal of Symbolic Logic 74 (1):279-314.
    We study satisfiability and infinite-state model checking in ICPDL, which extends Propositional Dynamic Logic (PDL) with intersection and converse operators on programs. The two main results of this paper are that (i) satisfiability is in 2EXPTIME, thus 2EXPTIME-complete by an existing lower bound, and (ii) infinite-state model checking of basic process algebras and pushdown systems is also 2EXPTIME-complete. Both upper bounds are obtained by polynomial time computable reductions to ω-regular tree satisfiability in ICPDL, a reasoning problem that we introduce specifically (...)
    Direct download (8 more)  
    Export citation  
    My bibliography  
  6.  2
    A Correspondence Between Temporal Description Logics.Alessandro Artale & Carsten Lutz - 2004 - Journal of Applied Non-Classical Logics 14 (1-2):209-233.
  7.  2
    A Complete System of Four-Valued Logic.P. H. Rodenburg & Carsten Lutz - 2001 - Journal of Applied Non-Classical Logics 11 (3-4):367-392.