Martin Lück ; Miikka Vilander - On the Succinctness of Atoms of Dependency

lmcs:5263 - Logical Methods in Computer Science, August 20, 2019, Volume 15, Issue 3 - https://doi.org/10.23638/LMCS-15(3:17)2019
On the Succinctness of Atoms of DependencyArticle

Authors: Martin Lück ; Miikka Vilander ORCID

    Propositional team logic is the propositional analog to first-order team logic. Non-classical atoms of dependence, independence, inclusion, exclusion and anonymity can be expressed in it, but for all atoms except dependence only exponential translations are known. In this paper, we systematically compare their succinctness in the existential fragment, where the splitting disjunction only occurs positively, and in full propositional team logic with unrestricted negation. By introducing a variant of the Ehrenfeucht-Fra\"{i}ssé game called formula size game into team logic, we obtain exponential lower bounds in the existential fragment for all atoms. In the full fragment, we present polynomial upper bounds also for all atoms.


    Volume: Volume 15, Issue 3
    Published on: August 20, 2019
    Accepted on: July 16, 2019
    Submitted on: March 7, 2019
    Keywords: Computer Science - Logic in Computer Science,68Q17, 03B60, 03B70,F.4.1
    Funding:
      Source : OpenAIRE Graph
    • Descriptive Complexity of Arithmetic Computations; Funder: Research Council of Finland; Code: 308099

    Consultation statistics

    This page has been seen 1629 times.
    This article's PDF has been downloaded 242 times.