arXiv subjects

Agi Kurucz

Publications and source records attributed to Agi Kurucz.

14 recordsLinked to original sources

arXiv2026

A non-uniform view of Craig interpolation in modal logics with linear frames

Normal modal logics extending the logic K4.3 of linear transitive frames are known to lack the Craig interpolation property, except some logics of bounded depth such as S5. We turn this `negative' fact into a research question and pursue a non-uniform approach to Craig interpolation by investigating the following interpolant existence problem: decide whether there exists a Craig interpolant between two given formulas in any fixed logic above K4.3. Using a bisimulation-based characterisation of interpolant existence for descriptive frames, we show that this problem is decidable and coNP-complete for all finitely axiomatisable normal modal logics containing K4.3. It is thus not harder than entailment in these logics, which is in sharp contrast to other recent non-uniform interpolation results. We also extend our approach to Priorean temporal logics (with both past and future modalities) over the standard time flows-the integers, rationals, reals, and finite strict linear orders-none of which is blessed with the Craig interpolation property.

math.LO↗

arXiv2025

From Interpolating Formulas to Separating Languages and Back Again

Traditionally, research on Craig interpolation is concerned with (a) establishing the Craig interpolation property (CIP) of a logic saying that every valid implication in the logic has a Craig interpolant and (b) designing algorithms that extract Craig interpolants from proofs. Logics that lack the CIP are regarded as `pathological' and excluded from consideration. In this chapter, we survey variations and generalisations of traditional Craig interpolation. First, we consider Craig interpolants for implications in logics without the CIP, focusing on the decidability and complexity of deciding their existence. We then generalise interpolation by looking for Craig interpolants in languages L' that can be weaker than the language L of the given implication. Thus, do not only we restrict the non-logical symbols of Craig interpolants but also the logical ones. The resulting L/L'-interpolation problem generalises L/L'-definability, the question whether an L-formula is equivalent to some L'-formula. After that, we move from logical languages to formal languages where interpolation disguises itself as separation: given two disjoint languages in a class C, does there exist a separating language in a smaller class C'? This question is particularly well-studied in the case when the input languages are regular and the separating language is first-order definable. Finally, we connect the different research strands by showing how the decidability of the separation problem for regular languages can be used to prove the decidability of Craig interpolant existence for linear temporal logic LTL.

cs.LO↗

arXiv2025

Deciding the Existence of Interpolants and Definitions in First-Order Modal Logic

None of the first-order modal logics between $\mathsf{K}$ and $\mathsf{S5}$ under the constant domain semantics enjoys Craig interpolation or projective Beth definability, even in the language restricted to a single individual variable. It follows that the existence of a Craig interpolant for a given implication or of an explicit definition for a given predicate cannot be directly reduced to validity as in classical first-order and many other logics. Our concern here is the decidability and computational complexity of the interpolant and definition existence problems. We first consider two decidable fragments of first-order modal logic $\mathsf{S5}$: the one-variable fragment $\mathsf{Q^1S5}$ and its extension $\mathsf{S5}_{\mathcal{ALC}^u}$ that combines $\mathsf{S5}$ and the description logic$\mathcal{ALC}$ with the universal role. We prove that interpolant and definition existence in $\mathsf{Q^1S5}$ and $\mathsf{S5}_{\mathcal{ALC}^u}$ is decidable in coN2ExpTime, being 2ExpTime-hard, while uniform interpolant existence is undecidable. These results transfer to the two-variable fragment $\mathsf{FO^2}$ of classical first-order logic without equality. We also show that interpolant and definition existence in the one-variable fragment $\mathsf{Q^1K}$ of first-order modal logic $\mathsf{K}$ is non-elementary decidable, while uniform interpolant existence is again undecidable.

cs.LO↗

arXiv2024

The interpolant existence problem for weak K4 and difference logic

As well known, weak K4 and the difference logic DL do not enjoy the Craig interpolation property. Our concern here is the problem of deciding whether any given implication does have an interpolant in these logics. We show that the nonexistence of an interpolant can always be witnessed by a pair of bisimilar models of polynomial size for DL and of triple-exponential size for weak K4, and so the interpolant existence problems for these logics are decidable in coNP and coN3ExpTime, respectively. We also establish coNExpTime-hardness of this problem for weak K4, which is higher than the PSpace-completeness of its decision problem.

cs.LO↗

arXiv2023

Deciding FO-rewritability of regular languages and ontology-mediated queries in Linear Temporal Logic

Our concern is the problem of determining the data complexity of answering an ontology-mediated query (OMQ) formulated in linear temporal logic LTL over (Z,<) and deciding whether it is rewritable to an FO(<)-query, possibly with some extra predicates. First, we observe that, in line with the circuit complexity and FO-definability of regular languages, OMQ answering in AC^0, ACC^0 and NC^1 coincides with FO(<,\equiv)-rewritability using unary predicates x \equiv 0 (mod n), FO(<,MOD)-rewritability, and FO(RPR)-rewritability using relational primitive recursion, respectively. We prove that, similarly to known PSPACE-completeness of recognising FO(<)-definability of regular languages, deciding FO(<,\equiv)- and FO(<,MOD)-definability is also \PSPACE-complete (unless ACC^0 = NC^1). We then use this result to show that deciding FO(<)-, FO(<,\equiv)- and FO(<,MOD)-rewritability of LTL OMQs is EXPSPACE-complete, and that these problems become PSPACE-complete for OMQs with a linear Horn ontology and an atomic query, and also a positive query in the cases of FO(<)- and FO(<,\equiv)-rewritability. Further, we consider FO(<)-rewritability of OMQs with a binary-clause ontology and identify OMQ classes, for which deciding it is PSPACE-, Pi_2^p- and coNP-complete.

cs.CC↗

arXiv2022

A tetrachotomy of ontology-mediated queries with a covering axiom

Our concern is the problem of efficiently determining the data complexity of answering queries mediated by description logic ontologies and constructing their optimal rewritings to standard database queries. Originated in ontology-based data access and datalog optimisation, this problem is known to be computationally very complex in general, with no explicit syntactic characterisations available. In this article, aiming to understand the fundamental roots of this difficulty, we strip the problem to the bare bones and focus on Boolean conjunctive queries mediated by a simple covering axiom stating that one class is covered by the union of two other classes. We show that, on the one hand, these rudimentary ontology-mediated queries, called disjunctive sirups (or d-sirups), capture many features and difficulties of the general case. For example, answering d-sirups is Pi^p_2-complete for combined complexity and can be in AC0 or LogSpace-, NL-, P-, or coNP-complete for data complexity (with the problem of recognising FO-rewritability of d-sirups being 2ExpTime-hard); some d-sirups only have exponential-size resolution proofs, some only double-exponential-size positive existential FO-rewritings and single-exponential-size nonrecursive datalog rewritings. On the other hand, we prove a few partial sufficient and necessary conditions of FO- and (symmetric/linear-) datalog rewritability of d-sirups. Our main technical result is a complete and transparent syntactic AC0/NL/P/coNP tetrachotomy of d-sirups with disjoint covering classes and a path-shaped Boolean conjunctive query. To obtain this tetrachotomy, we develop new techniques for establishing P- and coNP-hardness of answering non-Horn ontology-mediated queries as well as showing that they can be answered in NL.

cs.AI↗

arXiv2021

Deciding FO-definability of regular languages

We prove that, similarly to known PSpace-completeness of recognising FO(<)-definability of the language L(A) of a DFA A, deciding both FO(<,C)- and FO(<,MOD)-definability are PSpace-complete. (Here, FO(<,C) extends the first-order logic FO(<) with the standard congruence modulo n relation, and FO(<,MOD) with the quantifiers checking whether the number of positions satisfying a given formula is divisible by a given n>1. These FO-languages are known to define regular languages that are decidable in AC0 and ACC0, respectively.) We obtain these results by first showing that known algebraic characterisations of FO-definability of L(A) can be captured by `localisable' properties of the transition monoid of A. Using our criterion, we then generalise the known proof of PSpace-hardness of FO(<)-definability, and establish the upper bounds not only for arbitrary DFAs but also for two-way NFAs.

cs.LO↗

arXiv2021

Deciding boundedness of monadic sirups

We show that deciding boundedness (aka FO-rewritability) of monadic single rule datalog programs (sirups) is 2Exp-hard, which matches the upper bound known since 1988 and finally settles a long-standing open problem. We obtain this result as a byproduct of an attempt to classify monadic `disjunctive sirups' -- Boolean conjunctive queries q with unary and binary predicates mediated by a disjunctive rule T(x)vF(x) <- A(x) -- according to the data complexity of their evaluation. Apart from establishing that deciding FO-rewritability of disjunctive sirups with a dag-shaped q is also 2Exp-hard, we make substantial progress towards obtaining a complete FO/L-hardness dichotomy of disjunctive sirups with ditree-shaped q.

cs.CC↗

arXiv2020

Non-finitely axiomatisable modal product logics with infinite canonical axiomatisations

Our concern is the axiomatisation problem for modal and algebraic logics that correspond to various fragments of two-variable first-order logic with counting quantifiers. In particular, we consider modal products with Diff, the propositional unimodal logic of the difference operator. We show that the two-dimensional product logic Diff x Diff is non-finitely axiomatisable, but can be axiomatised by infinitely many Sahlqvist axioms. We also show that its `square' version (the modal counterpart of the substitution and equality free fragment of two-variable first-order logic with counting to two) is non-finitely axiomatisable over Diff x Diff, but can be axiomatised by adding infinitely many Sahlqvist axioms. These are the first examples of products of finitely axiomatisable modal logics that are not finitely axiomatisable, but axiomatisable by explicit infinite sets of canonical axioms.

cs.LO↗

arXiv2019

Kripke Completeness of Strictly Positive Modal Logics over Meet-semilattices with Operators

Our concern is the completeness problem for spi-logics, that is, sets of implications between strictly positive formulas built from propositional variables, conjunction and modal diamond operators. Originated in logic, algebra and computer science, spi-logics have two natural semantics: meet-semilattices with monotone operators providing Birkhoff-style calculi, and first-order relational structures (aka Kripke frames) often used as the intended structures in applications. Here we lay foundations for a completeness theory that aims to answer the question whether the two semantics define the same consequence relations for a given spi-logic.

cs.LO↗

arXiv2017

Horn Fragments of the Halpern-Shoham Interval Temporal Logic (Technical Report)

We investigate the satisfiability problem for Horn fragments of the Halpern-Shoham interval temporal logic depending on the type (box or diamond) of the interval modal operators, the type of the underlying linear order (discrete or dense), and the type of semantics for the interval relations (reflexive or irreflexive). For example, we show that satisfiability of Horn formulas with diamonds is undecidable for any type of linear orders and semantics. On the contrary, satisfiability of Horn formulas with boxes is tractable over both discrete and dense orders under the reflexive semantics and over dense orders under the irreflexive semantics, but becomes undecidable over discrete orders under the irreflexive semantics. Satisfiability of binary Horn formulas with both boxes and diamonds is always undecidable under the irreflexive semantics.

cs.LO↗

arXiv2015

The decision problem of modal product logics with a diagonal, and faulty counter machines

In the propositional modal (and algebraic) treatment of two-variable first-order logic equality is modelled by a `diagonal' constant, interpreted in square products of universal frames as the identity (also known as the `diagonal') relation. Here we study the decision problem of products of two arbitrary modal logics equipped with such a diagonal. As the presence or absence of equality in two-variable first-order logic does not influence the complexity of its satisfiability problem, one might expect that adding a diagonal to product logics in general is similarly harmless. We show that this is far from being the case, and there can be quite a big jump in complexity, even from decidable to the highly undecidable. Our undecidable logics can also be viewed as new fragments of first- order logic where adding equality changes a decidable fragment to undecidable. We prove our results by a novel application of counter machine problems. While our formalism apparently cannot force reliable counter machine computations directly, the presence of a unique diagonal in the models makes it possible to encode both lossy and insertion-error computations, for the same sequence of instructions. We show that, given such a pair of faulty computations, it is then possible to reconstruct a reliable run from them.

cs.LO↗

arXiv2015

Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting

First-order temporal logics are notorious for their bad computational behaviour. It is known that even the two-variable monadic fragment is highly undecidable over various linear timelines, and over branching time even one-variable fragments might be undecidable. However, there have been several attempts on finding well-behaved fragments of first-order temporal logics and related temporal description logics, mostly either by restricting the available quantifier patterns, or considering sub-Boolean languages. Here we analyse seemingly `mild' extensions of decidable one-variable fragments with counting capabilities, interpreted in models with constant, decreasing, and expanding first-order domains. We show that over most classes of linear orders these logics are (sometimes highly) undecidable, even without constant and function symbols, and with the sole temporal operator `eventually'. We establish connections with bimodal logics over 2D product structures having linear and `difference' (inequality) component relations, and prove our results in this bimodal setting. We show a general result saying that satisfiability over many classes of bimodal models with commuting linear and difference relations is undecidable. As a by-product, we also obtain new examples of finitely axiomatisable but Kripke incomplete bimodal logics. Our results generalise similar lower bounds on bimodal logics over products of two linear relations, and our proof methods are quite different from the proofs of these results. Unlike previous proofs that first `diagonally encode' an infinite grid, and then use reductions of tiling or Turing machine problems, here we make direct use of the grid-like structure of product frames and obtain undecidability by reductions of counter (Minsky) machine problems.

cs.LO↗

arXiv2015

Bimodal logics with a `weakly connected' component without the finite model property

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 fmp. Our results imply that the above positive result does not generalise to universally axiomatisable component logics, and even commutators without `transitive' components such as [K.3,K] can lack the fmp. We also generalise the above negative result to cases where one of the component logics has frames of depth one only, such as [S4.3,S5] and the decidable product logic S4.3xS5. We also show cases when already half of commutativity is enough to force infinite frames.

cs.LO↗