On the Succinctness of Atoms of Dependency

Miikka Vilander, Martin Lück

Research output: Contribution to journalArticleScientificpeer-review

1 Citation (Scopus)

Abstract

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.
Original languageEnglish
Pages (from-to)17:1-17:28
Number of pages28
JournalLogical Methods in Computer Science
Volume15
Issue number3
Publication statusPublished - 20 Aug 2019
Publication typeA1 Journal article-refereed

Keywords

  • team semantics
  • succinctness
  • dependence atom

Publication forum classification

  • Publication forum level 1

ASJC Scopus subject areas

  • Logic
  • Computational Theory and Mathematics

Fingerprint Dive into the research topics of 'On the Succinctness of Atoms of Dependency'. Together they form a unique fingerprint.

Cite this