On the complexity of team logic and its two-variable fragment

Show simple item record

dc.identifier.uri http://dx.doi.org/10.15488/4219
dc.identifier.uri https://www.repo.uni-hannover.de/handle/123456789/4253
dc.contributor.author Lück, Martin
dc.date.accessioned 2018-12-19T11:04:41Z
dc.date.available 2018-12-19T11:04:41Z
dc.date.issued 2018
dc.identifier.citation Lück, M.: On the complexity of team logic and its two-variable fragment. In: Leibniz International Proceedings in Informatics, LIPIcs 117 (2018), 27. DOI: https://doi.org/10.4230/LIPIcs.MFCS.2018.27
dc.description.abstract We study the logic FO(∼), the extension of first-order logic with team semantics by unrestricted Boolean negation. It was recently shown to be axiomatizable, but otherwise has not yet received much attention in questions of computational complexity. In this paper, we consider its two-variable fragment FO2(∼) and prove that its satisfiability problem is decidable, and in fact complete for the recently introduced non-elementary class TOWER(poly). Moreover, we classify the complexity of model checking of FO(∼) with respect to the number of variables and the quantifier rank, and prove a dichotomy between PSPACE- and ATIME-ALT(exp, poly)-complete fragments. For the lower bounds, we propose a translation from modal team logic MTL to FO2(∼) that extends the well-known standard translation from modal logic ML to FO2. For the upper bounds, we translate FO(∼) to fragments of second-order logic with PSPACE-complete and ATIME-ALT(exp, poly)-complete model checking, respectively. eng
dc.language.iso eng
dc.publisher Wadern : Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH
dc.relation.ispartofseries Leibniz International Proceedings in Informatics, LIPIcs 117 (2018)
dc.rights CC BY 4.0 Unported
dc.rights.uri https://creativecommons.org/licenses/by/4.0/
dc.subject Complexity eng
dc.subject Model checking eng
dc.subject Satisfiability eng
dc.subject Team logic eng
dc.subject Two-variable logic eng
dc.subject Model checking eng
dc.subject Semantics eng
dc.subject Complexity eng
dc.subject First order logic eng
dc.subject Satisfiability eng
dc.subject Satisfiability problems eng
dc.subject Second-order logic eng
dc.subject Team logic eng
dc.subject Two-variable logic eng
dc.subject Variable fragment eng
dc.subject Computer circuits eng
dc.subject.ddc 004 | Informatik ger
dc.title On the complexity of team logic and its two-variable fragment
dc.type article
dc.type conferenceObject
dc.type Text
dc.relation.issn 18688969
dc.relation.doi https://doi.org/10.4230/LIPIcs.MFCS.2018.27
dc.bibliographicCitation.volume 117
dc.bibliographicCitation.firstPage 27
dc.description.version publishedVersion
tib.accessRights frei zug�nglich


Files in this item

This item appears in the following Collection(s):

Show simple item record

 

Search the repository


Browse

My Account

Usage Statistics