We show that the guarded-negation fragment (GNFO) is, in a precise sense, the smallest extension of the guarded fragment (GFO) with Craig interpolation. In contrast, %we show that the smallest extension of the two-variable fragment (FO2) with Craig interpolation is full first-order logic.
In logics with the Craig interpolation property (CIP) the existence of an interpolant for an implication follows from the validity of the implication. In logics with the projective Beth definability property (PBDP), the existence of an explicit definition of a relation follows from the validity of a formula expressing its implicit definability. The two-variable fragment, FO2, and the guarded fragment, GF, of first-order logic both fail to have the CIP and the PBDP. We show that nevertheless in both fragments the existence of interpolants and explicit definitions is decidable. In GF, both probl…
In this paper we prove that the uniform one-dimensional guarded fragment, which is a natural polyadic generalization of the guarded two-variable logic, has the Craig interpolation property. We will also prove that the satisfiability problem of uniform guarded fragment is NEXPTIME-complete.
Answering Boolean conjunctive queries over the guarded fragment is decidable, however, as yet no practical decision procedure exists. Meanwhile, ordered resolution, as a practically oriented algorithm, is widely used in state-of-art modern theorem provers. In this paper, we devise a resolution decision procedure, which not only proves decidability of querying of the guarded fragment, but is implementable in any `off-the-shelf' resolution theorem prover with modest effort. Further, we extend the procedure to querying the loosely guarded fragment. The difficulty in querying a knowledge base of (…
We investigate the decidability and computational complexity of (deductive) conservative extensions in fragments of first-order logic (FO), with a focus on the two-variable fragment FO$^2$ and the guarded fragment GF. We prove that conservative extensions are undecidable in any FO fragment that contains FO$^2$ or GF (even the three-variable fragment thereof), and that they are decidable and 2\ExpTime-complete in the intersection GF$^2$ of FO$^2$ and GF.
In previous work, Abramsky, Dawar and Wang (LiCS 2017) and Abramsky and Shah (CSL 2018) have shown how a range of model comparison games which play a central role in finite model theory, including Ehrenfeucht-Fraisse, pebbling, and bisimulation games, can be captured in terms of resource-indexed comonads on the category of relational structures. Moreover, the coalgebras for these comonads capture important combinatorial parameters such as tree-width and tree-depth. The present paper extends this analysis to quantifier-guarded fragments of first-order logic. We give a systematic account, coveri…
We call a first-order formula one-dimensional if its every maximal block of existential (universal) quantifiers leaves at most one variable free. We consider the one-dimensional restrictions of the guarded fragment, GF, and the tri-guarded fragment, TGF, the latter being a recent extension of GF in which quantification for subformulas with at most two free variables need not be guarded, and which thus may be seen as a unification of GF and the two-variable fragment, FO2. We denote the resulting formalisms, resp., GF1, and TGF1. We show that GF1 has an exponential model property and NExpTime-co…
We consider the following query answering problem: Given a Boolean conjunctive query and a theory in the Horn loosely guarded fragment, the aim is to determine whether the query is entailed by the theory. In this paper, we present a resolution decision procedure for the loosely guarded fragment, and use such a procedure to answer Boolean conjunctive queries against the Horn loosely guarded fragment. The Horn loosely guarded fragment subsumes classes of rules that are prevalent in ontology-based query answering, such as Horn ALCHOI and guarded existential rules. Additionally, we identify star q…
The Guarded Negation Fragment (GNFO) is a fragment of first-order logic that contains all positive existential formulas, can express the first-order translations of basic modal logic and of many description logics, along with many sentences that arise in databases. It has been shown that the syntax of GNFO is restrictive enough so that computational problems such as validity and satisfiability are still decidable. This suggests that, in spite of its expressive power, GNFO formulas are amenable to novel optimizations. In this paper we study the model theory of GNFO formulas. Our results include…
We develop a doubly-exponential decision procedure for the satisfiability problem of guarded separation logic -- a novel fragment of separation logic featuring user-supplied inductive predicates, Boolean connectives, and separating connectives, including restricted (guarded) versions of negation, magic wand, and septraction. Moreover, we show that dropping the guards for any of the above connectives leads to an undecidable fragment. We further apply our decision procedure to reason about entailments in the popular symbolic heap fragment of separation logic. In particular, we obtain a doubly-ex…
Evaluating a Boolean conjunctive query Q against a guarded first-order theory F is equivalent to checking whether "F and not Q" is unsatisfiable. This problem is relevant to the areas of database theory and description logic. Since Q may not be guarded, well known results about the decidability, complexity, and finite-model property of the guarded fragment do not obviously carry over to conjunctive query answering over guarded theories, and had been left open in general. By investigating finite guarded bisimilar covers of hypergraphs and relational structures, and by substantially generalising…
The semijoin algebra is the variant of the relational algebra obtained by replacing the join operator by the semijoin operator. We discuss some interesting connections between the semijoin algebra and the guarded fragment of first-order logic. We also provide an Ehrenfeucht-Fraisse game, characterizing the discerning power of the semijoin algebra. This game gives a method for showing that certain queries are not expressible in the semijoin algebra.
Despite decades of research, there are still a number of concepts commonly found in software programs that are considered challenging for verification: among others, such concepts include concurrency, and the compositional analysis of programs with procedures. As a promising direction to overcome such difficulties, recently the use of Horn constraints as intermediate representation of software programs has been proposed. Horn constraints are related to Craig interpolation, which is one of the main techniques used to construct and refine abstractions in verification, and to synthesise inductive…
An important class of decidable first-order logic fragments are those satisfying a guardedness condition, such as the guarded fragment (GF). Usually, decidability for these logics is closely linked to the tree-like model property - the fact that satisfying models can be taken to have tree-like form. Decision procedures for the guarded fragment based on the tree-like model property are difficult to implement. An alternative approach, based on restricting first-order resolution, has been proposed, and this shows more promise from the point of view of implementation. In this work, we connect the …
Guarded Kleene Algebra with Tests (GKAT) is an efficient fragment of KAT, as it allows for almost linear decidability of equivalence. In this paper, we study the (co)algebraic properties of GKAT. Our initial focus is on the fragment that can distinguish between unsuccessful programs performing different actions, by omitting the so-called early termination axiom. We develop an operational (coalgebraic) and denotational (algebraic) semantics and show that they coincide. We then characterize the behaviors of GKAT expressions in this semantics, leading to a coequation that captures the covariety o…
University of Liverpool（利物浦大学）；University of Bremen（不来梅大学）
We study the complexity of ontology-mediated querying when ontologies are formulated in the guarded fragment of first-order logic (GF). Our general aim is to classify the data complexity on the level of ontologies where query evaluation w.r.t. an ontology O is considered to be in PTime if all (unions of conjunctive) queries can be evaluated in PTime w.r.t. O and coNP-hard if at least one query is coNP-hard w.r.t. O. We identify several large and relevant fragments of GF that enjoy a dichotomy between PTime and coNP, some of them additionally admitting a form of counting. In fact, almost all on…
We consider the family of guarded and unguarded ordered logics, that constitute a recently rediscovered family of decidable fragments of first-order logic (FO), in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. While the complexities of their satisfiability problems are now well-established, their model theory, however, is poorly understood. Our paper aims to provide some insight into it. We start by providing suitable notions of bisimulation for ordered logics. We next employ bisimulations to compare the rela…
In this paper we introduce a cut-free sequent calculus for the alternation-free fragment of the modal $μ$-calculus. This system allows for cyclic proofs and uses a simple focus mechanism to control the unravelling of fixpoints along infinite branches. We show that the proof system is sound and complete and apply it to prove that the alternation-free fragment has the Craig interpolation property.
We consider an extension of the unary negation fragment of first-order logic in which arbitrarily many binary symbols may be required to be interpreted as equivalence relations. We show that this extension has the finite model property. More specifically, we show that every satisfiable formula has a model of at most doubly exponential size. We argue that the satisfiability (= finite satisfiability) problem for this logic is TwoExpTime-complete. We also transfer our results to a restricted variant of the guarded negation fragment with equivalence relations.
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.
Craig interpolation has emerged as an effective means of generating candidate program invariants. We present interpolation procedures for the theories of Presburger arithmetic combined with (i) uninterpreted predicates (QPA+UP), (ii) uninterpreted functions (QPA+UF) and (iii) extensional arrays (QPA+AR). We prove that none of these combinations can be effectively interpolated without the use of quantifiers, even if the input formulae are quantifier-free. We go on to identify fragments of QPA+UP and QPA+UF with restricted forms of guarded quantification that are closed under interpolation. Form…
We study fragments of first-order logic and of least fixed point logic that allow only unary negation: negation of formulas with at most one free variable. These logics generalize many interesting known formalisms, including modal logic and the $μ$-calculus, as well as conjunctive queries and monadic Datalog. We show that satisfiability and finite satisfiability are decidable for both fragments, and we pinpoint the complexity of satisfiability, finite satisfiability, and model checking. We also show that the unary negation fragment of first-order logic is model-theoretically very well behaved.…
