This paper examines the complexity of hybrid logics over transitive frames, transitive trees, and linear frames. We show that satisfiability over transitive frames for the hybrid language extended with the downarrow operator is NEXPTIME-complete. This is in contrast to undecidability of satisfiability over arbitrary frames for this language (Areces, Blackburn, Marx 1999). It is also shown that adding the @ operator or the past modality leads to undecidability over transitive frames. This is again in contrast to the case of transitive trees and linear frames, where we show these languages to be nonelementarily decidable. Moreover, we establish 2EXPTIME and EXPTIME upper bounds for satisfiability over transitive frames and transitive trees, respectively, for the hybrid Until/Since language. An EXPTIME lower bound is shown to hold for the modal Until language over both frame classes.
This paper is focused on the study of modal logics defined from valued Kripke frames, and particularly, on computability and expressibility questions of modal logics of transitive Kripke frames evaluated over certain residuated lattices. It is shown that a large family of those logics -- including the ones arising from the standard MV and Product algebras -- yields an undecidable consequence relation. Later on, the behaviour of transitive modal Lukasiewicz logic is compared with that of its non transitive counterpart, exhibiting some particulars concerning computability and equivalence with ot…
Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of the transitive closure operator uniformly captures all finitary inductive definitions. In this paper we present an infinitary proof system for transitive closure logic which is an infinite descent-style counterpart to the existing (explicit induction) proof system for the logic. We show that, as for similar systems for first-ord…
The paper studies problems of satisfiability, decidability and admissibility of inference rules, conceptions of knowledge and agent's knowledge in non-transitive temporal linear logic LTL(Past,m). We find algorithms solving mentioned problems, justify our approach to consider linear non-transitive time with several examples. Main, most complicated, technical new result is decidability of LTL(Past,m) w.r.t. admissible rules. We discuss several ways to formalize conceptions of knowledge and agent's knowledge within given approach in non-transitive linear logic with models directed to past.
The finite model property of quasi-transitive modal logic $\mathsf{K}_2^3=\mathsf{K}\oplus \Box\Box p\rightarrow \Box\Box\Box p$ is established. This modal logic is conservatively extended to the tense logic $\mathsf{Kt}_2^3$. We present a Gentzen sequent calculus $\mathsf{G}$ for $\mathsf{Kt}_2^3$. The sequent calculus $\mathsf{G}$ has the finite algebra property by a finite syntactic construction. It follows that $\mathsf{Kt}_2^3$ and $\mathsf{K}_2^3$ have the finite model property.
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…
We propose a cut-free cyclic system for Transitive Closure Logic (TCL) based on a form of hypersequents, suitable for automated reasoning via proof search. We show that previously proposed sequent systems are cut-free incomplete for basic validities from Kleene Algebra (KA) and Propositional Dynamic Logic (PDL), over standard translations. On the other hand, our system faithfully simulates known cyclic systems for KA and PDL, thereby inheriting their completeness results. A peculiarity of our system is its richer correctness criterion, exhibiting 'alternating traces' and necessitating a more i…
Second-order transitive-closure logic, SO(TC), is an expressive declarative language that captures the complexity class PSPACE. Already its monadic fragment, MSO(TC), allows the expression of various NP-hard and even PSPACE-hard problems in a natural and elegant manner. As SO(TC) offers an attractive framework for expressing properties in terms of declaratively specified computations, it is interesting to understand the expressivity of different features of the language. This paper focuses on the fragment MSO(TC), as well on the purely existential fragment SO(2TC)(E); in 2TC, the TC operator b…
We introduce the branching transitive closure operator on weighted monadic second-order logic formulas where the branching corresponds in a natural way to the branching inherent in trees. For arbitrary commutative semirings, we prove that weighted monadic second order logics on trees is equivalent to the definability by formulas which start with one of the following operators: (i) a branching transitive closure or (ii) an existential second-order quantifier followed by one universal first-order quantifier; in both cases the operator is applied to step-formulas over (a) Boolean first-order logi…
In a previous paper, a tableau calculus has been presented, which constitute a decision procedure for hybrid logic with the converse and global modalities and a restricted use of the binder. This work extends such a calculus to multi-modal logic with transitive relations and relation inclusion assertions. The separate addition of either transitive relations or relation hierarchies to the considered decidable fragment of multi-modal hybrid logic can easily be shown to stay decidable, by resorting to results already proved in the literature. However, such results do not directly allow for conclu…
We study the satisfiability problem for the fluted fragment extended with transitive relations. We show that the logic enjoys the finite model property when only one transitive relation is available. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations.
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 study multimodal logics over universally first-order definable classes of frames. We show that even for bimodal logics, there are universal Horn formulas that define set of frames such that the satisfiability problem is undecidable, even if one or two of the binary relations are transitive.
While finite-variable fragments of the propositional modal logic S5--complete with respect to reflexive, symmetric and transitive frames--are polynomial-time decidable, the restriction to finite-variable formulas for logics of reflexive and transitive frames yields fragments that remain "intractable." The role of the symmetry condition in this context has not been investigated. We show that symmetry either by itself or in combination with reflexivity produces logics that behave just like logics of reflexive and transitive frames, i.e. their finite-variable fragments remain intractable, namely …
Kripke frames (and models) provide a suitable semantics for sub-classical logics, for example Intuitionistic Logic (of Brouwer and Heyting) axiomatizes the reflexive and transitive Kripke frames (with persistent satisfaction relations), and the Basic Logic (of Visser) axiomatizes transitive Kripke frames (with persistent satisfaction relations). Here, we investigate whether Kripke frames/models could provide a semantics for fuzzy logics. For each axiom of the Basic Fuzzy Logic, necessary and sufficient conditions are sought for Kripke frames/models which satisfy them. It turns out that the onl…
In previous works, a tableau calculus has been defined, which constitutes a decision procedure for hybrid logic with the converse and global modalities and a restricted use of the binder. This work shows how to extend such a calculus to multi-modal logic enriched with features largely used in description logics: transitivity and relation inclusion assertions. The separate addition of either transitive relations or relation hierarchies to the considered decidable fragment of multi-modal hybrid logic can easily be shown to stay decidable, by resorting to results already proved in the literature.…
We analyze the computational complexity of admissibility and unifiability with parameters in transitive modal logics. The class of cluster-extensible (clx) logics was introduced in the first part of this series of papers. We completely classify the complexity of unifiability or inadmissibility in any clx logic as being complete for one of $Σ^{\exp}_2$, NEXP, coNEXP, PSPACE, or $Π^p_2$. In addition to the main case where arbitrary parameters are allowed, we consider restricted problems with the number of parameters bounded by a constant, and the parameter-free case. Our upper bounds are specifi…
We show that the finite satisfiability problem for the unary negation fragment with arbitrary number of transitive relations is decidable and 2-ExpTime-complete. Our result actually holds for a more general setting in which one can require that some binary symbols are interpreted as arbitrary transitive relations, some as partial orders and some as equivalences. We also consider finite satisfiability of various extensions of our primary logic, in particular capturing the concepts of nominals and role hierarchies known from description logic. As the unary negation fragment can express unions of…
We give the first ExpTime (complexity-optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic SHOQ, which extends the basic description logic ALC with transitive roles, hierarchies of roles, nominals and quantified number restrictions. The complexity is measured using unary representation for numbers. Our procedure is based on global caching and integer linear feasibility checking.
We extend first-order logic with counting by a new operator that allows it to formalise a limited form of recursion which can be evaluated in logarithmic space. The resulting logic LREC has a data complexity in LOGSPACE, and it defines LOGSPACE-complete problems like deterministic reachability and Boolean formula evaluation. We prove that LREC is strictly more expressive than deterministic transitive closure logic with counting and incomparable in expressive power with symmetric transitive closure logic STC and transitive closure logic (with or without counting). LREC is strictly contained in …
We give the first cut-free ExpTime (optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic SHI, which extends the description logic ALC with transitive roles, inverse roles and role hierarchies.
University of Warsaw（华沙大学）；Cardiff University（卡迪夫大学）；University of Bremen（不来梅大学）
We study the description logic SQ with number restrictions applicable to transitive roles, extended with either nominals or inverse roles. We show tight 2EXPTIME upper bounds for unrestricted entailment of regular path queries for both extensions and finite entailment of positive existential queries for nominals. For inverses, we establish 2EXPTIME-completeness for unrestricted and finite entailment of instance queries (the latter under restriction to a single, transitive role).
We consider the satisfiability problem for the two-variable fragment of first-order logic over finite unranked trees. We work with signatures consisting of some unary predicates and the binary navigational predicates child, right sibling, and their respective transitive closures. We prove that the satisfiability problem for the logic containing all these predicates is EXPSPACE-complete. Further, we consider the restriction of the class of structures to singular trees, i.e., we assume that at every node precisely one unary predicate holds. We observe that the full logic and even for unordered t…
We consider a specific class of tree structures that can represent basic structures in linguistics and computer science such as XML documents, parse trees, and treebanks, namely, finite node-labeled sibling-ordered trees. We present axiomatizations of the monadic second-order logic (MSO), monadic transitive closure logic (FO(TC1)) and monadic least fixed-point logic (FO(LFP1)) theories of this class of structures. These logics can express important properties such as reachability. Using model-theoretic techniques, we show by a uniform argument that these axiomatizations are complete, i.e., eac…
We investigate the proof complexity of extended Frege (EF) systems for basic transitive modal logics (K4, S4, GL, ...) augmented with the bounded branching axioms $\mathbf{BB}_k$. First, we study feasibility of the disjunction property and more general extension rules in EF systems for these logics: we show that the corresponding decision problems reduce to total coNP search problems (or equivalently, disjoint NP pairs, in the binary case); more precisely, the decision problem for extension rules is equivalent to a certain special case of interpolation for the classical EF system. Next, we use…
There are two known general results on the finite model property (fmp) of commutators [L,L'] (bimodal logics with commuting and confluent modalities). If L is finitely axiomatisable by modal formulas having universal Horn first-order correspondents, then both [L,K] and [L,S5] are determined by classes of frames that admit filtration, and so have the fmp. On the negative side, if both L and L' are determined by transitive frames and have frames of arbitrarily large depth, then [L,L'] does not have the fmp. In this paper we show that commutators with a `weakly connected' component often lack the…
We introduce a description logic ALCQIO_{b,Re} which adds reachability assertions to ALCQIO, a sub-logic of the two-variable fragment of first order logic with counting quantifiers. ALCQIO_{b,Re} is well-suited for applications in software verification and shape analysis. Shape analysis requires expressive logics which can express reachability and have good computational properties. We show that ALCQIO_{b,Re} can describe complex data structures with a high degree of sharing and allows compositions such as list of trees. We show that the finite satisfiability and implication problems of ALCQIO…
We study model and frame definability of various modal logics. Let ML(A+) denote the fragment of modal logic extended with the universal modality in which the universal modality occurs only positively. We show that a class of Kripke models is definable in ML(A+) if and only if the class is elementary and closed under disjoint unions and surjective bisimulations. We also characterise the definability of ML(A+) in the spirit of the well-known Goldblatt--Thomason theorem. We show that an elementary class F of Kripke frames is definable in ML(A+) if and only if F is closed under taking generated s…
We study query answering in the description logic $\mathcal{SQ}$ supporting qualified number restrictions on both transitive and non-transitive roles. Our main contributions are a tree-like model property for $\mathcal{SQ}$ knowledge bases and, building upon this, an optimal automata-based algorithm for answering positive existential regular path queries in 2ExpTime.
We study probabilistic complexity classes and questions of derandomisation from a logical point of view. For each logic L we introduce a new logic BPL, bounded error probabilistic L, which is defined from L in a similar way as the complexity class BPP, bounded error probabilistic polynomial time, is defined from PTIME. Our main focus lies on questions of derandomisation, and we prove that there is a query which is definable in BPFO, the probabilistic version of first-order logic, but not in Cinf, finite variable infinitary logic with counting. This implies that many of the standard logics of f…
Birkbeck, University of London（伦敦大学伯贝克学院）；University of Oxford（牛津大学）；University of Warsaw（华沙大学）
We investigate the data complexity of answering queries mediated by metric temporal logic ontologies under the event-based semantics assuming that data instances are finite timed words timestamped with binary fractions. We identify classes of ontology-mediated queries answering which can be done in AC0, NC1, L, NL, P, and coNP for data complexity, provide their rewritings to first-order logic and its extensions with primitive recursion, transitive closure or datalog, and establish lower complexity bounds.
Institute of Computer Science University of Wrocław（弗罗茨瓦夫大学计算机科学研究所）；Technische Universität Dresden（德累斯顿工业大学）
The Triguarded Fragment (TGF) is among the most expressive decidable fragments of first-order logic, subsuming both its two-variable and guarded fragments without equality. We show that the TGF has the finite model property (providing a tight doubly exponential bound on the model size) and hence finite satisfiability coincides with satisfiability known to be N2ExpTime-complete. Using similar constructions, we also establish 2ExpTime-completeness for finite satisfiability of the constant-free (tri)guarded fragment with transitive guards.
The satisfiability problem of hybrid logics with the downarrow binder is known to be undecidable. This initiated a research program on decidable and tractable fragments. In this paper, we investigate the effect of restricting the propositional part of the language on decidability and on the complexity of the satisfiability problem over arbitrary, transitive, total frames, and frames based on equivalence relations. We also consider different sets of modal and hybrid operators. We trace the border of decidability and give the precise complexity of most fragments, in particular for all fragments …
Answering conjunctive queries (CQs) over $\mathcal{EL}$ knowledge bases (KBs) with complex role inclusions is PSPACE-hard and in PSPACE in certain cases; however, if complex role inclusions are restricted to role transitivity, the tight upper complexity bound has so far been unknown. Furthermore, the existing algorithms cannot handle reflexive roles, and they are not practicable. Finally, the problem is tractable for acyclic CQs and $\mathcal{ELH}$, and NP-complete for unrestricted CQs and $\mathcal{ELHO}$ KBs. In this paper we complete the complexity landscape of CQ answering for several impo…
Many tractable algorithms for solving the Constraint Satisfaction Problem (CSP) have been developed using the notion of the treewidth of some graph derived from the input CSP instance. In particular, the incidence graph of the CSP instance is one such graph. We introduce the notion of an incidence graph for modal logic formulae in a certain normal form. We investigate the parameterized complexity of modal satisfiability with the modal depth of the formula and the treewidth of the incidence graph as parameters. For various combinations of Euclidean, reflexive, symmetric and transitive models, w…
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 …
We propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct Sp(.) that captures the implicit supports of formulas -- the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on fram…
We investigate multi-agent epistemic modal logic with common knowledge modalities for groups of agents and obtain van Benthem style model-theoretic characterisations, in terms of bisimulation invariance of classical first-order logic over the non-elementary classes of (finite or arbitrary) common knowledge Kripke frames. The technical challenges posed by the reachability and transitive closure features of the derived accessibility relations are dealt with through passage to (finite) bisimilar coverings of epistemic frames by Cayley graphs of permutation groups whose generators are associated w…
We propose FC, a new logic on words that combines finite model theory with the theory of concatenation - a first-order logic that is based on word equations. Like the theory of concatenation, FC is built around word equations; in contrast to it, its semantics are defined to only allow finite models, by limiting the universe to a word and all its factors. As a consequence of this, FC has many of the desirable properties of FO on finite models, while being far more expressive than FO[<]. Most noteworthy among these desirable properties are sufficient criteria for efficient model checking, and ca…
An old theorem of Adámek constructs initial algebras for sufficiently cocontinuous endofunctors via transfinite iteration over ordinals in classical set theory. We prove a new version that works in constructive logic, using "inflationary" iteration over a notion of size that abstracts from limit ordinals just their transitive, directed and well-founded properties. Borrowing from Taylor's constructive treatment of ordinals, we show that sizes exist with upper bounds for any given signature of indexes. From this it follows that there is a rich class of endofunctors to which the new theorem appli…
