Switch to: References

Add citations

You must login to add citations.
  1. A New Framework for Epistemic Logic.Yanjing Wang - 2017 - In Proceedings of TARK 2017. EPTCS. pp. 515-534.
    Recent years witnessed a growing interest in non-standard epistemic logics of knowing whether, knowing how, knowing what, knowing why and so on. The new epistemic modalities introduced in those logics all share, in their semantics, the general schema of ∃x◻φ, e.g., knowing how to achieve φ roughly means that there exists a way such that you know that it is a way to ensure that φ. Moreover, the resulting logics are decidable. Inspired by those particular logics, in this work, we (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Combining linear-time temporal logic with constructiveness and paraconsistency.Norihiro Kamide & Heinrich Wansing - 2010 - Journal of Applied Logic 8 (1):33-61.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Epistemic logic.Vincent Hendricks - 2008 - Stanford Encyclopedia of Philosophy.
    Epistemic logic is the logic of knowledge and belief. It provides insight into the properties of individual knowers, has provided a means to model complicated scenarios involving groups of knowers and has improved our understanding of the dynamics of inquiry.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • 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 (...)
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Loosely guarded fragment of first-order logic has the finite model property.Ian Hodkinson - 2002 - Studia Logica 70 (2):205 - 240.
    We show that the loosely guarded and packed fragments of first-order logic have the finite model property. We use a construction of Herwig and Hrushovski. We point out some consequences in temporal predicate logic and algebraic logic.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Temporal logic.Temporal Logic - forthcoming - Stanford Encyclopedia of Philosophy.
    Download  
     
    Export citation  
     
    Bookmark  
  • 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 (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Monodic packed fragment with equality is decidable.Ian Hodkinson - 2002 - Studia Logica 72 (2):185-197.
    We prove decidability of satisfiability of sentences of the monodic packed fragment of first-order temporal logic with equality and connectives Until and Since, in models with various flows of time and domains of arbitrary cardinality. We also prove decidability over models with finite domains, over flows of time including the real order.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Refutation-Aware Gentzen-Style Calculi for Propositional Until-Free Linear-Time Temporal Logic.Norihiro Kamide - 2023 - Studia Logica 111 (6):979-1014.
    This study introduces refutation-aware Gentzen-style sequent calculi and Kripke-style semantics for propositional until-free linear-time temporal logic. The sequent calculi and semantics are constructed on the basis of the refutation-aware setting for Nelson’s paraconsistent logic. The cut-elimination and completeness theorems for the proposed sequent calculi and semantics are proven.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Essential and mandatory part-whole relations in conceptual data models.C. Maria Keet - unknown
    A recurring problem in conceptual modelling and ontology development is the representation of part-whole relations, with a requirement to be able to distinguish between essential and mandatory parts. To solve this problem, we formally characterize the semantics of these shareability notions by resorting to the temporal conceptual model E RVT and its formalization in the description logic DLRUS.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Temporal logic.Antony Galton - 2008 - Stanford Encyclopedia of Philosophy.
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Quantified epistemic logics for reasoning about knowledge in multi-agent systems.F. Belardinelli & A. Lomuscio - 2009 - Artificial Intelligence 173 (9-10):982-1013.
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Axiomatizing the monodic fragment of first-order temporal logic.Frank Wolter & Michael Zakharyaschev - 2002 - Annals of Pure and Applied Logic 118 (1-2):133-145.
    It is known that even seemingly small fragments of the first-order temporal logic over the natural numbers are not recursively enumerable. In this paper we show that the monodic fragment is an exception by constructing its finite Hilbert-style axiomatization. We also show that the monodic fragment with equality is not recursively axiomatizable.
    Download  
     
    Export citation  
     
    Bookmark   11 citations  
  • Temporal non-commutative logic: Expressing time, resource, order and hierarchy.Norihiro Kamide - 2009 - Logic and Logical Philosophy 18 (2):97-126.
    A first-order temporal non-commutative logic TN[l], which has no structural rules and has some l-bounded linear-time temporal operators, is introduced as a Gentzen-type sequent calculus. The logic TN[l] allows us to provide not only time-dependent, resource-sensitive, ordered, but also hierarchical reasoning. Decidability, cut-elimination and completeness (w.r.t. phase semantics) theorems are shown for TN[l]. An advantage of TN[l] is its decidability, because the standard first-order linear-time temporal logic is undecidable. A correspondence theorem between TN[l] and a resource indexed non-commutative logic RN[l] (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Undecidability of first-order intuitionistic and modal logics with two variables.Roman Kontchakov, Agi Kurucz & Michael Zakharyaschev - 2005 - Bulletin of Symbolic Logic 11 (3):428-438.
    We prove that the two-variable fragment of first-order intuitionistic logic is undecidable, even without constants and equality. We also show that the two-variable fragment of a quantified modal logic L with expanding first-order domains is undecidable whenever there is a Kripke frame for L with a point having infinitely many successors (such are, in particular, the first-order extensions of practically all standard modal logics like K, K4, GL, S4, S5, K4.1, S4.2, GL.3, etc.). For many quantified modal logics, including those (...)
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Propositional Epistemic Logics with Quantification Over Agents of Knowledge (An Alternative Approach).Gennady Shtakser - 2019 - Studia Logica 107 (4):753-780.
    In the previous paper with a similar title :311–344, 2018), we presented a family of propositional epistemic logics whose languages are extended by two ingredients: by quantification over modal operators or over agents of knowledge and by predicate symbols that take modal operators as arguments. We denoted this family by \}\). The family \}\) is defined on the basis of a decidable higher-order generalization of the loosely guarded fragment of first-order logic. And since HO-LGF is decidable, we obtain the decidability (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Variations on the Kripke Trick.Mikhail Rybakov & Dmitry Shkatov - forthcoming - Studia Logica:1-48.
    In the early 1960s, to prove undecidability of monadic fragments of sublogics of the predicate modal logic $$\textbf{QS5}$$ QS 5 that include the classical predicate logic $$\textbf{QCl}$$ QCl, Saul Kripke showed how a classical atomic formula with a binary predicate letter can be simulated by a monadic modal formula. We consider adaptations of Kripke’s simulation, which we call the Kripke trick, to various modal and superintuitionistic predicate logics not considered by Kripke. We also discuss settings where the Kripke trick does (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • On the axiomatizability of some first-order spatio-temporal theories.Sándor Vályi - 2015 - Synthese 192 (7):1-17.
    Spatio-temporal logic is a variant of branching temporal logic where one of the so-called causal relations on spacetime plays the role of a time flow. Allowing only rational numbers as space and time co-ordinates, we prove that a first-order spatio-temporal theory over this flow is recursively enumerable if and only if the dimension of spacetime does not exceed 2. The situation is somewhat different compared to the case of real co-ordinates, because we establish that even dimension 2 does not permit (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • First-order expressivity for s5-models: Modal vs. two-sorted languages.Holger Sturm & Frank Wolter - 2001 - Journal of Philosophical Logic 30 (6):571-591.
    Standard models for model predicate logic consist of a Kripke frame whose worlds come equipped with relational structures. Both modal and two-sorted predicate logic are natural languages for speaking about such models. In this paper we compare their expressivity. We determine a fragment of the two-sorted language for which the modal language is expressively complete on S5-models. Decidable criteria for modal definability are presented.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Bounded linear-time temporal logic: A proof-theoretic investigation.Norihiro Kamide - 2012 - Annals of Pure and Applied Logic 163 (4):439-466.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • The serializability problem for a temporal logic of transaction queries.Walter Hussak - 2008 - Journal of Applied Non-Classical Logics 18 (1):67-78.
    We define the logic FOTLT(n), to be a monadic monodic fragment of first-order linear temporal logic, with 2n propositions representing the read and write steps of n two-step concurrent database transactions and a time-dependent predicate representing queries giving the sets of data items accessed by those read and write steps at given points in time. The models of FOTLT(n) contain interleaved sequences of the steps of infinitely many occurrences of the n transactions accessing unlimited data over time. A property of (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Decidable Cases of First-order Temporal Logic with Functions.Walter Hussak - 2008 - Studia Logica 88 (2):247-261.
    We consider the decision problem for cases of first-order temporal logic with function symbols and without equality. The monadic monodic fragment with flexible functions can be decided with EXPSPACE-complete complexity. A single rigid function is sufficient to make the logic not recursively enumerable. However, the monadic monodic fragment with rigid functions, where no two distinct terms have variables bound by the same quantifier, is decidable and EXPSPACE-complete.
    Download  
     
    Export citation  
     
    Bookmark  
  • Complexity of monodic guarded fragments over linear and real time.Ian Hodkinson - 2006 - Annals of Pure and Applied Logic 138 (1):94-125.
    We show that the satisfiability problem for the monodic guarded, loosely guarded, and packed fragments of first-order temporal logic with equality is 2Exptime-complete for structures with arbitrary first-order domains, over linear time, dense linear time, rational number time, and some other classes of linear flows of time. We then show that for structures with finite first-order domains, these fragments are also 2Exptime-complete over real number time and hence over most of the commonly used linear flows of time, including the natural (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Constraint LTL satisfiability checking without automata.Marcello M. Bersani, Achille Frigeri, Angelo Morzenti, Matteo Pradella, Matteo Rossi & Pierluigi San Pietro - 2014 - Journal of Applied Logic 12 (4):522-557.
    Download  
     
    Export citation  
     
    Bookmark