arXiv subjects

Juha Kontinen

Publications and source records attributed to Juha Kontinen.

At least 37 records · Page 2Linked to original sources

arXiv2023

Regular Representations of Uniform TC^0

The circuit complexity class DLOGTIME-uniform AC^0 is known to be a modest subclass of DLOGTIME-uniform TC^0. The weakness of AC^0 is caused by the fact that AC^0 is not closed under restricting AC^0-computable queries into simple subsequences of the input. Analogously, in descriptive complexity, the logics corresponding to DLOGTIME-uniform AC^0 do not have the relativization property and hence they are not regular. This weakness of DLOGTIME-uniform AC^0 has been elaborated in the line of research on the Crane Beach Conjecture. The conjecture (which was refuted by Barrington, Immerman, Lautemann, Schweikardt and Th{é}rien) was that if a language L has a neutral letter, then L can be defined in first-order logic with the collection of all numerical built-in relations, if and only if L can be already defined in FO with order. In the first part of this article we consider logics in the range of AC^0 and TC^0. First we formulate a combinatorial criterion for a cardinality quantifier C_S implying that all languages in DLOGTIME-uniform TC^0 can be defined in FO(C_S). For instance, this criterion is satisfied by C_S if S is the range of some polynomial with positive integer coefficients of degree at least two. In the second part of the paper we first adapt the key properties of abstract logics to accommodate built-in relations. Then we define the regular interior R-int(L) and regular closure R-cl(L), of a logic L, and show that the Crane Beach Conjecture can be interpreted as a statement concerning the regular interior of first-order logic with built-in relations B. We show that if B={+}, or B contains only unary relations besides the order, then R-int(FO_B) collapses to FO with order. In contrast, our results imply that if B contains the order and the range of a polynomial of degree at least two, then R-cl(FO_B) includes all languages in DLOGTIME-uniform TC^0.

cs.LO↗

arXiv2023

Complexity of Neural Network Training and ETR: Extensions with Effectively Continuous Functions

We study the complexity of the problem of training neural networks defined via various activation functions. The training problem is known to be existsR-complete with respect to linear activation functions and the ReLU activation function. We consider the complexity of the problem with respect to the sigmoid activation function and other effectively continuous functions. We show that these training problems are polynomial-time many-one bireducible to the existential theory of the reals extended with the corresponding activation functions. In particular, we establish that the sigmoid activation function leads to the existential theory of the reals with the exponential function. It is thus open, and equivalent with the decidability of the existential theory of the reals with the exponential function, whether training neural networks using the sigmoid activation function is algorithmically solvable. In contrast, we obtain that the training problem is undecidable if sinusoidal activation functions are considered. Finally, we obtain general upper bounds for the complexity of the training problem in the form of low levels of the arithmetical hierarchy.

cs.LO↗

arXiv2023

Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity

We introduce and develop a set-based semantics for asynchronous TeamLTL. We consider two canonical logics in this setting: the extensions of TeamLTL by the Boolean disjunction and by the Boolean negation. We establish fascinating connections between the original semantics based on multisets and the new set-based semantics as well as show one of the first positive complexity theoretic results in the temporal team semantics setting. In particular we show that both logics enjoy normal forms that can be utilised to obtain results related to expressivity and complexity (decidability) of the new logics. We also relate and apply our results to recently defined logics whose asynchronicity is formalized via time evaluation functions.

cs.LO↗

arXiv2023

Unified Foundations of Team Semantics via Semirings

Semiring semantics for first-order logic provides a way to trace how facts represented by a model are used to deduce satisfaction of a formula. Team semantics is a framework for studying logics of dependence and independence in diverse contexts such as databases, quantum mechanics, and statistics by extending first-order logic with atoms that describe dependencies between variables. Combining these two, we propose a unifying approach for analysing the concepts of dependence and independence via a novel semiring team semantics, which subsumes all the previously considered variants for first-order team semantics. In particular, we study the preservation of satisfaction of dependencies and formulae between different semirings. In addition we create links to reasoning tasks such as provenance, counting, and repairs.

cs.LO↗

arXiv2023

Parameterized Complexity of Weighted Team Definability

In this article, we study the complexity of weighted team definability for logics with team semantics. This problem is a natural analogue of one of the most studied problems in parameterized complexity, the notion of weighted Fagin-definability, which is formulated in terms of satisfaction of first-order formulas with free relation variables. We focus on the parameterized complexity of weighted team definability for a fixed formula phi of central team-based logics. Given a first-order structure A and the parameter value k as input, the question is to determine whether A,T models phi for some team T of size k. We show several results on the complexity of this problem for dependence, independence, and inclusion logic formulas. Moreover, we also relate the complexity of weighted team definability to the complexity classes in the well-known W-hierarchy as well as paraNP.

cs.LO↗

arXiv2022

Complete logics for elementary team properties

In this paper, we introduce a logic based on team semantics, called FOT, whose expressive power is elementary, i.e., coincides with first-order logic both on the level of sentences and (possibly open) formulas, and we also show that a sublogic of FOT, called FOT${}^\downarrow$, captures exactly downward closed elementary (or first-order) team properties. We axiomatize completely the logic FOT, and also extend the known partial axiomatization of dependence logic to dependence logic enriched with the logical constants in FOT${}^\downarrow$.

math.LO↗

arXiv2022

Modular SAT-based techniques for reasoning tasks in team semantics

We study the complexity of reasoning tasks for logics in team semantics. Our main focus is on the data complexity of model checking but we also derive new results for logically defined counting and enumeration problems. Our approach is based on modular reductions of these problems into the corresponding problems of various classes of Boolean formulas. We illustrate our approach via several new tractability/intractability results.

cs.LO↗

arXiv2021

Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity

We study the expressivity and complexity of model checking linear temporal logic with team semantics (TeamLTL). TeamLTL, despite being a purely modal logic, is capable of defining hyperproperties, i.e., properties which relate multiple execution traces. TeamLTL has been introduced quite recently and only few results are known regarding its expressivity and its model checking problem. We relate the expressivity of TeamLTL to logics for hyperproperties obtained by extending LTL with trace and propositional quantifiers (HyperLTL and HyperQPTL). By doing so, we obtain a number of model checking results for TeamLTL and identify its undecidability frontier. In particular, we show decidability of model checking of the so-called left-flat fragment of any downward closed TeamLTL-extension. Moreover, we establish that the model checking problem of TeamLTL with Boolean disjunction and inclusion atoms is undecidable.

cs.LO↗

arXiv2021

On the Expressive Power of TeamLTL and First-Order Team Logic over Hyperproperties

In this article we study linear temporal logics with team semantics (TeamLTL) that are novel logics for defining hyperproperties. We define Kamp-type translations of these logics into fragments of first-order team logic and second-order logic. We also characterize the expressive power and the complexity of model-checking and satisfiability of team logic and second-order logic by relating them to second- and third-order arithmetic. Our results set in a larger context the recent results of Lück showing that the extension of TeamLTL by the Boolean negation is highly undecidable under the so-called synchronous semantics. We also study stutter-invariant fragments of extensions of TeamLTL.

cs.LO↗

arXiv2021

A Parameterized View on the Complexity of Dependence Logic

In this paper, we investigate the parameterized complexity of model checking for Dependence Logic which is a well studied logic in the area of Team Semantics. We start with a list of nine immediate parameterizations for this problem, namely: the number of disjunctions (i.e., splits)/(free) variables/universal quantifiers, formula-size, the tree-width of the Gaifman graph of the input structure, the size of the universe/team, and the arity of dependence atoms. We present a comprehensive picture of the parameterized complexity of model checking and obtain a division of the problem into tractable and various intractable degrees. Furthermore, we also consider the complexity of the most important variants (data and expression complexity) of the model checking problem by fixing parts of the input.

cs.LO↗

arXiv2021

Tractability Frontier of Data Complexity in Team Semantics

We study the data complexity of model-checking for logics with team semantics. We focus on dependence, inclusion, and independence logic formulas under both strict and lax team semantics. Our results delineate a clear tractability/intractability frontiers in data complexity of both quantifier-free and quantified formulas for each of the logics. For inclusion logic under the lax semantics, we reduce the model-checking problem to the satisfiability problem of so-called dual-Horn Boolean formulas. Via this reduction, we give an alternative proof for the known result that the data complexity of inclusion logic is in PTIME.

cs.LO↗

arXiv2021

On elementary logics for quantitative dependencies

We define and study logics in the framework of probabilistic team semantics and over metafinite structures. Our work is paralleled by the recent development of novel axiomatizable and tractable logics in team semantics that are closed under the Boolean negation. Our logics employ new probabilistic atoms that resemble so-called extended atoms from the team semantics literature. We also define counterparts of our logics over metafinite structures and show that all of our logics can be translated into functional fixed point logic implying a polynomial time upper bound for data complexity with respect to BSS-computations.

cs.LO↗

arXiv2021

On the Interaction of Functional and Inclusion Dependencies with Independence Atoms

Infamously, the finite and unrestricted implication problems for the classes of i) functional and inclusion dependencies together, and ii) embedded multivalued dependencies alone are each undecidable. Famously, the restriction of i) to functional and unary inclusion dependencies in combination with the restriction of ii) to multivalued dependencies yield implication problems that are still different in the finite and unrestricted case, but each are finitely axiomatizable and decidable in low-degree polynomial time. An important embedded tractable fragment of embedded multivalued dependencies are independence atoms that stipulate independence between two attribute sets. We establish a series of results for implication problems over subclasses of the combined class of functional and inclusion dependencies as well as independence atoms. One of our main results is that both finite and unrestricted implication problems for the combined class of independence atoms, unary functional and unary inclusion dependencies are axiomatizable and decidable in low-degree polynomial time.

cs.DB↗

arXiv2020

Counting of Teams in First-Order Team Logics

We study descriptive complexity of counting complexity classes in the range from #P to #$\cdot$NP. A corollary of Fagin's characterization of NP by existential second-order logic is that #P can be logically described as the class of functions counting satisfying assignments to free relation variables in first-order formulae. In this paper we extend this study to classes beyond #P and extensions of first-order logic with team semantics. These team-based logics are closely related to existential second-order logic and its fragments, hence our results also shed light on the complexity of counting for extensions of FO in Tarski's semantics. Our results show that the class #$\cdot$NP can be logically characterized by independence logic and existential second-order logic, whereas dependence logic and inclusion logic give rise to subclasses of #$\cdot$NP and #P , respectively. Our main technical result shows that the problem of counting satisfying assignments for monotone Boolean $Σ_1$-formulae is #$\cdot$NP-complete as well as complete for the function class generated by dependence logic.

cs.LO↗

arXiv2020

On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic

Second-order Boolean logic is a generalization of QBF, whose constant alternation fragments are known to be complete for the levels of the exponential time hierarchy. We consider two types of restriction of this logic: 1) restrictions to term constructions, 2) restrictions to the form of the Boolean matrix. Of the first sort, we consider two kinds of restrictions: firstly, disallowing nested use of proper function variables, and secondly stipulating that each function variable must appear with a fixed sequence of arguments. Of the second sort, we consider Horn, Krom, and core fragments of the Boolean matrix. We classify the complexity of logics obtained by combining these two types of restrictions. We show that, in most cases, logics with k alternating blocks of function quantifiers are complete for the kth or (k-1)th level of the exponential time hierarchy. Furthermore, we establish NL-completeness for the Krom and core fragments, when k=1 and both restrictions of the first sort are in effect.

cs.LO↗

arXiv2020

Descriptive complexity of real computation and probabilistic independence logic

We introduce a novel variant of BSS machines called Separate Branching BSS machines (S-BSS in short) and develop a Fagin-type logical characterisation for languages decidable in non-deterministic polynomial time by S-BSS machines. We show that NP on S-BSS machines is strictly included in NP on BSS machines and that every NP language on S-BSS machines is a countable union of closed sets in the usual topology of R^n. Moreover, we establish that on Boolean inputs NP on S-BSS machines without real constants characterises a natural fragment of the complexity class existsR (a class of problems polynomial time reducible to the true existential theory of the reals) and hence lies between NP and PSPACE. Finally we apply our results to determine the data complexity of probabilistic independence logic.

cs.LO↗

arXiv2020

Polyteam Semantics

Team semantics is the mathematical framework of modern logics of dependence and independence in which formulae are interpreted by sets of assignments (teams) instead of single assignments as in first-order logic. In order to deepen the fruitful interplay between team semantics and database dependency theory, we define "Polyteam Semantics" in which formulae are evaluated over a family of teams. We begin by defining a novel polyteam variant of dependence atoms and give a finite axiomatisation for the associated implication problem. We relate polyteam semantics to team semantics and investigate in which cases logics over the former can be simulated by logics over the latter. We also characterise the expressive power of poly-dependence logic by properties of polyteams that are downwards closed and definable in existential second-order logic (ESO). The analogous result is shown to hold for poly-independence logic and all ESO-definable properties. We also relate poly-inclusion logic to greatest fixed point logic.

cs.LO↗

arXiv2019

Facets of Distribution Identities in Probabilistic Team Semantics

We study probabilistic team semantics which is a semantical framework allowing the study of logical and probabilistic dependencies simultaneously. We examine and classify the expressive power of logical formalisms arising by different probabilistic atoms such as conditional independence and different variants of marginal distribution equivalences. We also relate the framework to the first-order theory of the reals and apply our methods to the open question on the complexity of the implication problem of conditional independence.

cs.LO↗