Search Results

Documents authored by Virtema, Jonni

Document
DOI: 10.4230/DagRep.14.3.31
Logics for Dependence and Independence: Expressivity and Complexity (Dagstuhl Seminar 24111)

Authors: Juha Kontinen, Jonni Virtema, Heribert Vollmer, Fan Yang, and Nicolas Fröhlich

Published in: Dagstuhl Reports, Volume 14, Issue 3 (2024)

Abstract
This report documents the programme and outcomes of Dagstuhl Seminar "Logics for Dependence and Independence: Expressivity and Complexity" (24111). This seminar served as a follow-up seminar to the highly successful seminars "Dependence Logic: Theory and Applications" (13071), "Logics for Dependence and Independence" (15261) and "Logics for Dependence and Independence" (19031). A key objective of the seminar was to bring together researchers working in dependence logic and in application areas (for this edition with a particular emphasis on the areas of hyperproperties and formal linguistics), so that they can communicate state-of-the-art advances and embark on a systematic interaction. The goal was especially to reach those researchers who have recently started working in this thriving area, as well as researchers working on several aspects of complexity studies of team-based logics as well as expressivity issues, in particular in the just mentioned application areas. In particular, bringing together researchers from areas of theoretical studies with the application areas aimed at enhancing the synergy between the different communities working on dependence logic.
Cite as

Juha Kontinen, Jonni Virtema, Heribert Vollmer, Fan Yang, and Nicolas Fröhlich. Logics for Dependence and Independence: Expressivity and Complexity (Dagstuhl Seminar 24111). In Dagstuhl Reports, Volume 14, Issue 3, pp. 31-51, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{kontinen_et_al:DagRep.14.3.31,
  author =	{Kontinen, Juha and Virtema, Jonni and Vollmer, Heribert and Yang, Fan and Fr\"{o}hlich, Nicolas},
  title =	{{Logics for Dependence and Independence: Expressivity and Complexity (Dagstuhl Seminar 24111)}},
  pages =	{31--51},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{14},
  number =	{3},
  editor =	{Kontinen, Juha and Virtema, Jonni and Vollmer, Heribert and Yang, Fan and Fr\"{o}hlich, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.3.31},
  URN =		{urn:nbn:de:0030-drops-211827},
  doi =		{10.4230/DagRep.14.3.31},
  annote =	{Keywords: finite model theory, formal linguistics, hyperproperties, information theory, team semantics}
}
Document
DOI: 10.4230/LIPIcs.CSL.2024.15
Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals

Authors: Fausto Barbero and Jonni Virtema

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
Causal multiteam semantics is a framework where probabilistic dependencies arising from data and causation between variables can be together formalized and studied logically. We discover complete characterizations of expressivity for several logics that can express probabilistic statements, conditioning and interventionist counterfactuals. The results characterize the languages in terms of families of linear equations and closure conditions that define the corresponding classes of causal multiteams. The characterizations yield a strict hierarchy of expressive power. Finally, we present some undefinability results based on the characterizations.
Cite as

Fausto Barbero and Jonni Virtema. Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{barbero_et_al:LIPIcs.CSL.2024.15,
  author =	{Barbero, Fausto and Virtema, Jonni},
  title =	{{Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{15:1--15:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.15},
  URN =		{urn:nbn:de:0030-drops-196583},
  doi =		{10.4230/LIPIcs.CSL.2024.15},
  annote =	{Keywords: Interventionist counterfactuals, Multiteam semantics, Causation, Probability logic, Linear inequalities, Expressive power}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2023.60
Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity

Authors: Juha Kontinen, Max Sandström, and Jonni Virtema

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
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 relate the new semantics with the original semantics based on multisets and establish 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.
Cite as

Juha Kontinen, Max Sandström, and Jonni Virtema. Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 60:1-60:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kontinen_et_al:LIPIcs.MFCS.2023.60,
  author =	{Kontinen, Juha and Sandstr\"{o}m, Max and Virtema, Jonni},
  title =	{{Set Semantics for Asynchronous TeamLTL: Expressivity and Complexity}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{60:1--60:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.60},
  URN =		{urn:nbn:de:0030-drops-185949},
  doi =		{10.4230/LIPIcs.MFCS.2023.60},
  annote =	{Keywords: Hyperproperties, Linear Temporal Logic, Team Semantics}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2021.52
Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity

Authors: Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen, and Fan Yang

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract
We study the expressivity and complexity of model checking of 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.
Cite as

Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen, and Fan Yang. Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 52:1-52:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{virtema_et_al:LIPIcs.FSTTCS.2021.52,
  author =	{Virtema, Jonni and Hofmann, Jana and Finkbeiner, Bernd and Kontinen, Juha and Yang, Fan},
  title =	{{Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{52:1--52:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.52},
  URN =		{urn:nbn:de:0030-drops-155634},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.52},
  annote =	{Keywords: Linear temporal logic, Hyperproperties, Model Checking, Expressivity}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.27
On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic

Authors: Miika Hannula, Juha Kontinen, Martin Lück, and Jonni Virtema

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
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.
Cite as

Miika Hannula, Juha Kontinen, Martin Lück, and Jonni Virtema. On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 27:1-27:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{hannula_et_al:LIPIcs.CSL.2021.27,
  author =	{Hannula, Miika and Kontinen, Juha and L\"{u}ck, Martin and Virtema, Jonni},
  title =	{{On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{27:1--27:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.27},
  URN =		{urn:nbn:de:0030-drops-134610},
  doi =		{10.4230/LIPIcs.CSL.2021.27},
  annote =	{Keywords: quantified Boolean formulae, computational complexity, second-order logic, Horn and Krom fragment}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.22
Expressivity Within Second-Order Transitive-Closure Logic

Authors: Flavio Ferrarotti, Jan Van den Bussche, and Jonni Virtema

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Second-order transitive-closure logic, SO(TC), is an expressive declarative language that captures the complexity class PSPACE. Already its monadic fragment, MSO(TC), allows the expression of various NP-hard and even PSPACE-hard problems in a natural and elegant manner. As SO(TC) offers an attractive framework for expressing properties in terms of declaratively specified computations, it is interesting to understand the expressivity of different features of the language. This paper focuses on the fragment MSO(TC), as well on the purely existential fragment SO(2TC)(exists); in 2TC, the TC operator binds only tuples of relation variables. We establish that, with respect to expressive power, SO(2TC)(exists) collapses to existential first-order logic. In addition we study the relationship of MSO(TC) to an extension of MSO(TC) with counting features (CMSO(TC)) as well as to order-invariant MSO. We show that the expressive powers of CMSO(TC) and MSO(TC) coincide. Moreover we establish that, over unary vocabularies, MSO(TC) strictly subsumes order-invariant MSO.
Cite as

Flavio Ferrarotti, Jan Van den Bussche, and Jonni Virtema. Expressivity Within Second-Order Transitive-Closure Logic. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{ferrarotti_et_al:LIPIcs.CSL.2018.22,
  author =	{Ferrarotti, Flavio and Van den Bussche, Jan and Virtema, Jonni},
  title =	{{Expressivity Within Second-Order Transitive-Closure Logic}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{22:1--22:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.22},
  URN =		{urn:nbn:de:0030-drops-96896},
  doi =		{10.4230/LIPIcs.CSL.2018.22},
  annote =	{Keywords: Expressive power, Higher order logics, Descriptive complexity}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.10
Team Semantics for the Specification and Verification of Hyperproperties

Authors: Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
We develop team semantics for Linear Temporal Logic (LTL) to express hyperproperties, which have recently been identified as a key concept in the verification of information flow properties. Conceptually, we consider an asynchronous and a synchronous variant of team semantics. We study basic properties of this new logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of these basic logics react on adding other atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL under team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties.
Cite as

Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann. Team Semantics for the Specification and Verification of Hyperproperties. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{krebs_et_al:LIPIcs.MFCS.2018.10,
  author =	{Krebs, Andreas and Meier, Arne and Virtema, Jonni and Zimmermann, Martin},
  title =	{{Team Semantics for the Specification and Verification of Hyperproperties}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{10:1--10:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.10},
  URN =		{urn:nbn:de:0030-drops-95926},
  doi =		{10.4230/LIPIcs.MFCS.2018.10},
  annote =	{Keywords: LTL, Hyperproperties, Team Semantics, Model Checking, Satisfiability}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.32
Model Checking and Validity in Propositional and Modal Inclusion Logics

Authors: Lauri Hella, Antti Kuusisto, Arne Meier, and Jonni Virtema

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
Propositional and modal inclusion logic are formalisms that belong to the family of logics based on team semantics. This article investigates the model checking and validity problems of these logics. We identify complexity bounds for both problems, covering both lax and strict team semantics. By doing so, we come close to finalising the programme that ultimately aims to classify the complexities of the basic reasoning problems for modal and propositional dependence, independence, and inclusion logics.
Cite as

Lauri Hella, Antti Kuusisto, Arne Meier, and Jonni Virtema. Model Checking and Validity in Propositional and Modal Inclusion Logics. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 32:1-32:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{hella_et_al:LIPIcs.MFCS.2017.32,
  author =	{Hella, Lauri and Kuusisto, Antti and Meier, Arne and Virtema, Jonni},
  title =	{{Model Checking and Validity in Propositional and Modal Inclusion Logics}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{32:1--32:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.32},
  URN =		{urn:nbn:de:0030-drops-81007},
  doi =		{10.4230/LIPIcs.MFCS.2017.32},
  annote =	{Keywords: Inclusion Logic, Model Checking, Complexity}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2016.60
Decidability of Predicate Logics with Team Semantics

Authors: Juha Kontinen, Antti Kuusisto, and Jonni Virtema

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)

Abstract
We study the complexity of predicate logics based on team semantics. We show that the satisfiability problems of two-variable independence logic and inclusion logic are both NEXPTIME-complete. Furthermore, we show that the validity problem of two-variable dependence logic is undecidable, thereby solving an open problem from the team semantics literature. We also briefly analyse the complexity of the Bernays-Schoenfinkel-Ramsey prefix classes of dependence logic.
Cite as

Juha Kontinen, Antti Kuusisto, and Jonni Virtema. Decidability of Predicate Logics with Team Semantics. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 60:1-60:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{kontinen_et_al:LIPIcs.MFCS.2016.60,
  author =	{Kontinen, Juha and Kuusisto, Antti and Virtema, Jonni},
  title =	{{Decidability of Predicate Logics with Team Semantics}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{60:1--60:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.60},
  URN =		{urn:nbn:de:0030-drops-64726},
  doi =		{10.4230/LIPIcs.MFCS.2016.60},
  annote =	{Keywords: team semantics, dependence logic, complexity, two-variable logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.292
Axiomatizing Propositional Dependence Logics

Authors: Katsuhiko Sano and Jonni Virtema

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
We give sound and complete Hilbert-style axiomatizations for propositional dependence logic (PD), modal dependence logic (MDL), and extended modal dependence logic (EMDL) by extending existing axiomatizations for propositional logic and modal logic. In addition, we give novel labeled tableau calculi for PD, MDL, and EMDL. We prove soundness, completeness and termination for each of the labeled calculi.
Cite as

Katsuhiko Sano and Jonni Virtema. Axiomatizing Propositional Dependence Logics. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 292-307, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{sano_et_al:LIPIcs.CSL.2015.292,
  author =	{Sano, Katsuhiko and Virtema, Jonni},
  title =	{{Axiomatizing Propositional Dependence Logics}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{292--307},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.292},
  URN =		{urn:nbn:de:0030-drops-54215},
  doi =		{10.4230/LIPIcs.CSL.2015.292},
  annote =	{Keywords: propositional dependence logic, modal dependence logic, axiomatization, tableau calculus}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.470
Undecidable First-Order Theories of Affine Geometries

Authors: Antti Kuusisto, Jeremy Meyers, and Jonni Virtema

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
Tarski initiated a logic-based approach to formal geometry that studies first-order structures with a ternary betweenness relation (\beta) and a quaternary equidistance relation (\equiv). Tarski established, inter alia, that the first-order (FO) theory of (R^2,\beta,\equiv) is decidable. Aiello and van Benthem (2002) conjectured that the FO-theory of expansions of (R^2,\beta) with unary predicates is decidable. We refute this conjecture by showing that for all n > 1, the FO-theory of monadic expansions of (R^n,\beta) is Pi^1_1-hard and therefore not even arithmetical. We also define a natural and comprehensive class C of geometric structures (T,\beta), where T is a subset of R^n, and show that for each structure (T,\beta) in C, the FO-theory of the class of monadic expansions of (T,\beta) is undecidable. We then consider classes of expansions of structures (T,\beta) with restricted unary predicates, for example finite predicates, and establish a variety of related undecidability results. In addition to decidability questions, we briefly study the expressivity of universal MSO and weak universal MSO over expansions of (R^n,\beta). While the logics are incomparable in general, over expansions of (R^n,\beta), formulae of weak universal MSO translate into equivalent formulae of universal MSO. An extended version of this article can be found on the ArXiv (arXiv:1208.4930v1).
Cite as

Antti Kuusisto, Jeremy Meyers, and Jonni Virtema. Undecidable First-Order Theories of Affine Geometries. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 470-484, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{kuusisto_et_al:LIPIcs.CSL.2012.470,
  author =	{Kuusisto, Antti and Meyers, Jeremy and Virtema, Jonni},
  title =	{{Undecidable First-Order Theories of Affine Geometries}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{470--484},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.470},
  URN =		{urn:nbn:de:0030-drops-36910},
  doi =		{10.4230/LIPIcs.CSL.2012.470},
  annote =	{Keywords: Tarski’s geometry, undecidability, spatial logic, classical logic}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact