Separation logic and its variants can describe various properties on pointer programs. However, when it comes to properties on sequences, one may find it hard to formalize. To deal with properties on variable-length sequences and multilevel data structures, we propose sequence-heap separation logic which integrates sequences into logical reasoning on heap-manipulated programs. Quantifiers over sequence variables and singleton heap storing sequence (sequence singleton heap) are new members in our logic. Further, we study the satisfiability problem of two fragments. The propositional fragment of sequence-heap separation logic is decidable, and the fragment with 2 alternations on program variables and 1 alternation on sequence variables is undecidable. In addition, we explore boundaries between decidable and undecidable fragments of the logic with prenex normal form.
We establish decidability for the infinitely many axiomatic extensions of the commutative Full Lambek logic with weakening FLew (i.e. IMALLW) that have a cut-free hypersequent proof calculus (specifically: every analytic structural rule extension). Decidability for the corresponding extensions of its contraction counterpart FLec was established recently but their computational complexity was left unanswered. In the second part of this paper, we introduce just enough on length functions for well-quasi-orderings and the fast-growing complexity classes to obtain complexity upper bounds for both t…
In this paper syntactic objects---concept constructors called part restrictions which realize rational grading are considered in Description Logics (DLs). Being able to convey statements about a rational part of a set of successors, part restrictions essentially enrich the expressive capabilities of DLs. We examine an extension of well-studied DL ALCQIHR+ with part restrictions, and prove that the reasoning in the extended logic is still decidable. The proof uses tableaux technique augmented with indices technique, designed for dealing with part restrictions.
Hyperproperties are properties of systems that relate different executions traces, with many applications from security to symmetry, consistency models of concurrency, etc. In recent years, different linear-time logics for specifying asynchronous hyperproperties have been investigated. Though model checking of these logics is undecidable, useful decidable fragments have been identified with applications e.g. for asynchronous security analysis. In this paper, we address expressiveness and decidability issues of temporal logics for asynchronous hyperproperties. We compare the expressiveness of t…
The aim of our paper is twofold: firstly we present a sequent calculus for an intuitionistic non-Fregean logic ISCI, which is based on the calculus presented in the paper by Chlebowski and Leszczynska-Jasion, 'An Investigation into Intuitionistic Logic with Identity' (Bulletin of the Section of Logic 48(4), p. 259-283, 2019) and, secondly, we discuss the problem of decidability of ISCI via the obtained system. The original calculus from the mentioned paper did not provide the decidability result for ISCI. There are two problems to be solved in order to obtain this result: the so called loops c…
On the Decidability and Complexity of Some Fragments of Metric Temporal Logic
度量时态逻辑$\mtlfull$是研究最多的实时逻辑之一。它表现出相当大的多样性的表达性和可判定性的基础上允许的一套模式和时间间隔的限制$I$的性质。\oomit{The classical results of Alur and Henzinger showed that $\mtlfull$ is undecidable where as $\mitl$ which uses only non-singular intervals $NS$ is decidable. In a surprizing result, Ouaknine and Worrell showed that the satisfiability of $\mtl$ is decidable over finite pointwise models, albeit with NPR decision complexity, whereas it remains undecidable for infinite pointwise models or for continuous time.}在本文中，我们通过证明$\mtlsns$（其中$NS$表示非奇异区间）的可满足性在有限逐点严格单调时间上也是可判定的，从而加强了可判定性结果。我们利用时间投影技术给出了从Ouaknine和Worrell的逻辑$\mtls…
Decidability of the Clark's Completion Semantics for Monadic Programs and Queries
对于一般的逻辑程序（即在子句主体中使用否定的程序），有许多不同的语义。这些语义中的大多数是图灵完备的（在某种意义上可以精确化），这意味着它们是不可判定的。为了获得可判定性，需要对程序和查询施加额外的限制。在逻辑编程中，对底层的一阶语言施加限制是很自然的。在本说明中，我们展示了一元一般程序和查询的克拉克完成语义的可判定性。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
We investigate the complexity consequences of adding pointer arithmetic to separation logic. Specifically, we study extensions of the points-to fragment of symbolic-heap separation logic with various forms of Presburger arithmetic constraints. Most significantly, we find that, even in the minimal case when we allow only conjunctions of simple "difference constraints" (x'\leq x+k) where k is an integer, polynomial-time decidability is already impossible: satisfiability becomes NP-complete, while quantifier-free entailment becomes coNP-complete and quantified entailment becomes P2-complete (P2 i…
We consider dynamic versions of epistemic logic as formulated in Baltag and Moss "Logics for epistemic programs" (2004). That paper proposed a logical language (actually families of languages parameterized by action signatures) for dynamic epistemic logic. It had been shown that validity in the language is Pi-1-1-complete, so there are no recursively axiomatized complete logical systems for it. In contrast, this paper proves a weak completeness result for the fragment without action iteration, and a strong completeness result for the fragment without action iteration and common knowledge. Our …
Alternating-time Temporal Logic (ATL*) is a central logic for multiagent systems. Its extension to the imperfect information setting (ATL*i ) is well known to have an undecidable model-checking problem when agents have perfect recall. Studies have thus mostly focused either on agents without memory, or on alternative semantics to retrieve decidability. In this work we establish new decidability results for agents with perfect recall: We first prove a meta-theorem that allows the transfer of decidability results for classes of multiplayer games with imperfect information, such as games with hie…
We consider first-order logic over the subword ordering on finite words, where each word is available as a constant. Our first result is that the $Σ_1$ theory is undecidable (already over two letters). We investigate the decidability border by considering fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over languages with a bounded number of letter alternations. We prove that when at most two variables are not alternation bounded, the $Σ_1$ fragment is decidable, and that it becomes undecidable when three variab…
Institute of Mathematical Sciences, Homi Bhabha National Institute（数学科学研究所，霍米·巴巴国家研究所）；Peking University（北京大学）
Quantified modal logic provides a natural logical language for reasoning about modal attitudes even while retaining the richness of quantification for referring to predicates over domains. But then most fragments of the logic are undecidable, over many model classes. Over the years, only a few fragments (such as the monodic) have been shown to be decidable. In this paper, we study fragments that bundle quantifiers and modalities together, inspired by earlier work on epistemic logics of know-how/why/what. As always with quantified modal logics, it makes a significant difference whether the doma…
This work proposes a Dynamic Epistemic Logic with Communication Actions that can be performed concurrently. Unlike Concurrent Epistemic Action Logic introduced by Ditmarsch, Hoek and Kooi, where the concurrency mechanism is the so called true concurrency, here we use an approach based on process calculus, like CCS and CSP, and Action Models Logic. Our approach makes possible the proof of soundness, completeness and decidability, different from the others approaches. We present an axiomatization and show that the proof of soundness, completeness and decidability can be done using a reduction me…
This work provides proof-search algorithms and automated counter-model extraction for a class of STIT logics. With this, we answer an open problem concerning syntactic decision procedures and cut-free calculi for STIT logics. A new class of cut-free complete labelled sequent calculi G3LdmL^m_n, for multi-agent STIT with at most n-many choices, is introduced. We refine the calculi G3LdmL^m_n through the use of propagation rules and demonstrate the admissibility of their structural rules, resulting in auxiliary calculi Ldm^m_nL. In the single-agent case, we show that the refined calculi Ldm^m_nL…
Self-extensional logics of formal inconsistency: Decidability and limits for paraconsistency
Centre for Logic, Epistemology and the History of Science (CLE), University of Campinas (UNICAMP)（坎皮纳斯大学逻辑、认识论与科学史中心）；Institute of Philosophy and the Humanities (IFCH), University of Campinas (UNICAMP)（坎皮纳斯大学哲学与人文学院）
We develop an inductive proof-technique to generate imperative programs for pointer data structures from behavioural specifications expressed in the Answer Set Programming (ASP) formalism. ASP is a non-monotonic logic based formalism that employs negation-as-failure which helps emulate the human thought process, allowing domain experts to model desired system behaviour succinctly. We argue in this paper that ASP's reliance on negation-as-failure makes it a better formalism than those based on first-order logic for writing formal specifications. We assume the a domain expert provides the repres…
Most Properties are Undecidable for Transitive Tense Logics
The Tsinghua-UvA JRC for Logic Department of Philosophy Tsinghua University（清华大学哲学系清华-阿姆斯特丹逻辑联合研究中心）；Institute for Logic, Language and Computation University of Amsterdam（阿姆斯特丹大学逻辑、语言与计算研究所）
We introduce an extension of Strategy Logic for the imperfect-information setting, called SLii, and study its model-checking problem. As this logic naturally captures multi-player games with imperfect information, the problem turns out to be undecidable. We introduce a syntactical class of "hierarchical instances" for which, intuitively, as one goes down the syntactic tree of the formula, strategy quantifications are concerned with finer observations of the model. We prove that model-checking SLii restricted to hierarchical instances is decidable. This result, because it allows for complex pat…
We study the satisfiability problem for the two-variable first-order logic over structures with one transitive relation. % We show that the problem is decidable in 2-NExpTime for the fragment consisting of formulas where existential quantifiers are guarded by transitive atoms. As this fragment enjoys neither the finite model nor the tree model property, to show decidability we introduce novel model construction technique based on the infinite Ramsey theorem. We also point out why the technique is not sufficient to obtain decidability for the full two-variable logic with one transitive relation…
