12 Search Results for "Th�rien, Denis"


Document
10061 Abstracts Collection – Circuits, Logic, and Games

Authors: Benjamin Rossman, Thomas Schwentick, Denis Thérien, and Heribert Vollmer

Published in: Dagstuhl Seminar Proceedings, Volume 10061, Circuits, Logic, and Games (2010)


Abstract
From 07/02/10 to 12/02/10, the Dagstuhl Seminar 10061 ``Circuits, Logic, and Games '' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Benjamin Rossman, Thomas Schwentick, Denis Thérien, and Heribert Vollmer. 10061 Abstracts Collection – Circuits, Logic, and Games. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 10061, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{rossman_et_al:DagSemProc.10061.1,
  author =	{Rossman, Benjamin and Schwentick, Thomas and Th\'{e}rien, Denis and Vollmer, Heribert},
  title =	{{10061 Abstracts Collection – Circuits, Logic, and Games}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10061},
  editor =	{Benjamin Rossman and Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10061.1},
  URN =		{urn:nbn:de:0030-drops-25280},
  doi =		{10.4230/DagSemProc.10061.1},
  annote =	{Keywords: Computational complexity theory, Finite model theory, Boolean circuits, Regular languages, Finite monoids, Ehrenfeucht-Fra\{\backslash''i\}ss\'{e}-games}
}
Document
10061 Executive Summary – Circuits, Logic, and Games

Authors: Benjamin Rossman, Thomas Schwentick, Denis Thérien, and Heribert Vollmer

Published in: Dagstuhl Seminar Proceedings, Volume 10061, Circuits, Logic, and Games (2010)


Abstract
In the same way as during the first seminar on "Circuits, Logic, and Games"(Nov.~2006, 06451), the organizers aimed to bring together researchers from the areas of finite model theory and computational complexity theory, since they felt that perhaps not all developments in circuit theory and in logic had been explored fully in the context of lower bounds. In fact, the interaction between the areas has flourished a lot in the past 2-3 years, as can be exemplified by the following lines of research.

Cite as

Benjamin Rossman, Thomas Schwentick, Denis Thérien, and Heribert Vollmer. 10061 Executive Summary – Circuits, Logic, and Games. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 10061, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{rossman_et_al:DagSemProc.10061.2,
  author =	{Rossman, Benjamin and Schwentick, Thomas and Th\'{e}rien, Denis and Vollmer, Heribert},
  title =	{{10061 Executive Summary – Circuits, Logic, and Games}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--5},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10061},
  editor =	{Benjamin Rossman and Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10061.2},
  URN =		{urn:nbn:de:0030-drops-25279},
  doi =		{10.4230/DagSemProc.10061.2},
  annote =	{Keywords: Computational complexity theory, finite model theory, Boolean circuits, regular languages, finite monoids, Ehrenfeucht-Fra\backslash"\backslashi ss\backslash'e-games}
}
Document
Complexity Results for Modal Dependence Logic

Authors: Peter Lohmann and Heribert Vollmer

Published in: Dagstuhl Seminar Proceedings, Volume 10061, Circuits, Logic, and Games (2010)


Abstract
Modal dependence logic was introduced very recently by Väänänen. It enhances the basic modal language by an operator dep. For propositional variables p_1,...,p_n, dep(p_1,...,p_(n-1);p_n) intuitively states that the value of p_n only depends on those of p_1,...,p_(n-1). Sevenster (J. Logic and Computation, 2009) showed that satisfiability for modal dependence logic is complete for nondeterministic exponential time. In this paper we consider fragments of modal dependence logic obtained by restricting the set of allowed propositional connectives. We show that satisfibility for poor man's dependence logic, the language consisting of formulas built from literals and dependence atoms using conjunction, necessity and possibility (i.e., disallowing disjunction), remains NEXPTIME-complete. If we only allow monotone formulas (without negation, but with disjunction), the complexity drops to PSPACE-completeness. We also extend Väänänen's language by allowing classical disjunction besides dependence disjunction and show that the satisfiability problem remains NEXPTIME-complete. If we then disallow both negation and dependence disjunction, satistiability is complete for the second level of the polynomial hierarchy. In this way we completely classify the computational complexity of the satisfiability problem for all restrictions of propositional and dependence operators considered by Väänänen and Sevenster.

Cite as

Peter Lohmann and Heribert Vollmer. Complexity Results for Modal Dependence Logic. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 10061, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{lohmann_et_al:DagSemProc.10061.3,
  author =	{Lohmann, Peter and Vollmer, Heribert},
  title =	{{Complexity Results for Modal Dependence Logic}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10061},
  editor =	{Benjamin Rossman and Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10061.3},
  URN =		{urn:nbn:de:0030-drops-25240},
  doi =		{10.4230/DagSemProc.10061.3},
  annote =	{Keywords: Dependence logic, satisfiability problem, computational complexity, poor man's logic}
}
Document
Hardness of Parameterized Resolution

Authors: Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria

Published in: Dagstuhl Seminar Proceedings, Volume 10061, Circuits, Logic, and Games (2010)


Abstract
Parameterized Resolution and, moreover, a general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (FOCS'07). In that paper, Dantchev et al. show a complexity gap in tree-like Parameterized Resolution for propositional formulas arising from translations of first-order principles. We broadly investigate Parameterized Resolution obtaining the following main results: 1) We introduce a purely combinatorial approach to obtain lower bounds to the proof size in tree-like Parameterized Resolution. For this we devise a new asymmetric Prover-Delayer game which characterizes proofs in (parameterized) tree-like Resolution. By exhibiting good Delayer strategies we then show lower bounds for the pigeonhole principle as well as the order principle. 2) Interpreting a well-known FPT algorithm for vertex cover as a DPLL procedure for Parameterized Resolution, we devise a proof search algorithm for Parameterized Resolution and show that tree-like Parameterized Resolution allows short refutations of all parameterized contradictions given as bounded-width CNF's. 3) We answer a question posed by Dantchev, Martin, and Szeider showing that dag-like Parameterized Resolution is not fpt-bounded. We obtain this result by proving that the pigeonhole principle requires proofs of size $n^{Omega(k)}$ in dag-like Parameterized Resolution. For this lower bound we use a different Prover-Delayer game which was developed for Resolution by Pudlák.

Cite as

Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. Hardness of Parameterized Resolution. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 10061, pp. 1-28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:DagSemProc.10061.4,
  author =	{Beyersdorff, Olaf and Galesi, Nicola and Lauria, Massimo},
  title =	{{Hardness of Parameterized Resolution}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--28},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10061},
  editor =	{Benjamin Rossman and Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10061.4},
  URN =		{urn:nbn:de:0030-drops-25254},
  doi =		{10.4230/DagSemProc.10061.4},
  annote =	{Keywords: Proof complexity, parameterized complexity, Resolution, Prover-Delayer Games}
}
Document
Proof Complexity of Propositional Default Logic

Authors: Olaf Beyersdorff, Arne Meier, Sebastian Müller, Michael Thomas, and Heribert Vollmer

Published in: Dagstuhl Seminar Proceedings, Volume 10061, Circuits, Logic, and Games (2010)


Abstract
Default logic is one of the most popular and successful formalisms for non-monotonic reasoning. In 2002, Bonatti and Olivetti introduced several sequent calculi for credulous and skeptical reasoning in propositional default logic. In this paper we examine these calculi from a proof-complexity perspective. In particular, we show that the calculus for credulous reasoning obeys almost the same bounds on the proof size as Gentzen's system LK. Hence proving lower bounds for credulous reasoning will be as hard as proving lower bounds for LK. On the other hand, we show an exponential lower bound to the proof size in Bonatti and Olivetti's enhanced calculus for skeptical default reasoning.

Cite as

Olaf Beyersdorff, Arne Meier, Sebastian Müller, Michael Thomas, and Heribert Vollmer. Proof Complexity of Propositional Default Logic. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 10061, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:DagSemProc.10061.5,
  author =	{Beyersdorff, Olaf and Meier, Arne and M\"{u}ller, Sebastian and Thomas, Michael and Vollmer, Heribert},
  title =	{{Proof Complexity of Propositional Default Logic}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--14},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10061},
  editor =	{Benjamin Rossman and Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10061.5},
  URN =		{urn:nbn:de:0030-drops-25261},
  doi =		{10.4230/DagSemProc.10061.5},
  annote =	{Keywords: Proof complexity, default logic, sequent calculus}
}
Document
The Complexity of Reasoning for Fragments of Autoepistemic Logic

Authors: Nadia Creignou, Arne Meier, Michael Thomas, and Heribert Vollmer

Published in: Dagstuhl Seminar Proceedings, Volume 10061, Circuits, Logic, and Games (2010)


Abstract
Autoepistemic logic extends propositional logic by the modal operator L. A formula that is preceded by an L is said to be "believed". The logic was introduced by Moore 1985 for modeling an ideally rational agent's behavior and reasoning about his own beliefs. In this paper we analyze all Boolean fragments of autoepistemic logic with respect to the computational complexity of the three most common decision problems expansion existence, brave reasoning and cautious reasoning. As a second contribution we classify the computational complexity of counting the number of stable expansions of a given knowledge base. To the best of our knowledge this is the first paper analyzing the counting problem for autoepistemic logic.

Cite as

Nadia Creignou, Arne Meier, Michael Thomas, and Heribert Vollmer. The Complexity of Reasoning for Fragments of Autoepistemic Logic. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 10061, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{creignou_et_al:DagSemProc.10061.6,
  author =	{Creignou, Nadia and Meier, Arne and Thomas, Michael and Vollmer, Heribert},
  title =	{{The Complexity of Reasoning for Fragments of Autoepistemic Logic}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--10},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10061},
  editor =	{Benjamin Rossman and Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10061.6},
  URN =		{urn:nbn:de:0030-drops-25234},
  doi =		{10.4230/DagSemProc.10061.6},
  annote =	{Keywords: Autoepistemic logic, computational complexity, nonmonotonic reasoning, Post's lattice}
}
Document
06451 Abstracts Collection – Circuits, Logic, and Games

Authors: Thomas Schwentick, Denis Thérien, and Heribert Vollmer

Published in: Dagstuhl Seminar Proceedings, Volume 6451, Circuits, Logic, and Games (2007)


Abstract
From 08.11.06 to 10.11.06, the Dagstuhl Seminar 06451 ``Circuits, Logic, and Games'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Thomas Schwentick, Denis Thérien, and Heribert Vollmer. 06451 Abstracts Collection – Circuits, Logic, and Games. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 6451, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{schwentick_et_al:DagSemProc.06451.1,
  author =	{Schwentick, Thomas and Th\'{e}rien, Denis and Vollmer, Heribert},
  title =	{{06451 Abstracts Collection – Circuits, Logic, and Games }},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--10},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6451},
  editor =	{Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06451.1},
  URN =		{urn:nbn:de:0030-drops-9785},
  doi =		{10.4230/DagSemProc.06451.1},
  annote =	{Keywords: Computational complexity theory, finite model theory, Boolean circuits, regular languages, finite monoids, Ehrenfeucht-Fra\backslash"\{\backslashi\}ss\backslash'\{e\} games}
}
Document
06451 Executive Summary – Circuits, Logic, and Games

Authors: Thomas Schwentick, Denis Thérien, and Heribert Vollmer

Published in: Dagstuhl Seminar Proceedings, Volume 6451, Circuits, Logic, and Games (2007)


Abstract
In this document we describe the original motivation and goals of the seminar as well as the sequence of talks given during the seminar.

Cite as

Thomas Schwentick, Denis Thérien, and Heribert Vollmer. 06451 Executive Summary – Circuits, Logic, and Games. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 6451, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{schwentick_et_al:DagSemProc.06451.2,
  author =	{Schwentick, Thomas and Th\'{e}rien, Denis and Vollmer, Heribert},
  title =	{{06451 Executive Summary – Circuits, Logic, and Games }},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6451},
  editor =	{Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06451.2},
  URN =		{urn:nbn:de:0030-drops-9774},
  doi =		{10.4230/DagSemProc.06451.2},
  annote =	{Keywords: Circuits, Logics, Games}
}
Document
A note on the size of Craig Interpolants

Authors: Uwe Schöning and Jacobo Torán

Published in: Dagstuhl Seminar Proceedings, Volume 6451, Circuits, Logic, and Games (2007)


Abstract
Mundici considered the question of whether the interpolant of two propositional formulas of the form $F ightarrow G$ can always have a short circuit description, and showed that if this is the case then every problem in NP $cap$ co-NP would have polynomial size circuits. In this note we observe further consequences of the interpolant having short circuit descriptions, namely that UP $subseteq$ P$/$poly, and that every single valued NP function has a total extension in FP$/$poly. We also relate this question with other Complexity Theory assumptions.

Cite as

Uwe Schöning and Jacobo Torán. A note on the size of Craig Interpolants. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 6451, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{schoning_et_al:DagSemProc.06451.3,
  author =	{Sch\"{o}ning, Uwe and Tor\'{a}n, Jacobo},
  title =	{{A note on the size of Craig Interpolants}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6451},
  editor =	{Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06451.3},
  URN =		{urn:nbn:de:0030-drops-9735},
  doi =		{10.4230/DagSemProc.06451.3},
  annote =	{Keywords: Interpolant, non-uniform complexity}
}
Document
Counting Results in Weak Formalisms

Authors: Arnaud Durand, Clemens Lautemann, and Malika More

Published in: Dagstuhl Seminar Proceedings, Volume 6451, Circuits, Logic, and Games (2007)


Abstract
The counting ability of weak formalisms is of interest as a measure of their expressive power. The question was investigated in the 1980's in several papers in complexity theory and in weak arithmetic. In each case, the considered formalism (AC$^0$--circuits, first--order logic, $Delta_0$, respectively) was shown to be able to count precisely up to a polylogarithmic number. An essential part of each of the proofs is the construction of a 1--1 mapping from a small subset of ${0,ldots,N-1}$ into a small initial segment. In each case the expressibility of such a mapping depends on some strong argument (group theoretic device or prime number theorem) or intricate construction. We present a coding device based on a collision-free hashing technique, leading to a completely elementary proof for the polylog counting capability of first--order logic (with built--in arithmetic), $AC^0$--circuits, rudimentary arithmetic, the Linear Hierarchy, and monadic--second order logic with addition.

Cite as

Arnaud Durand, Clemens Lautemann, and Malika More. Counting Results in Weak Formalisms. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 6451, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{durand_et_al:DagSemProc.06451.4,
  author =	{Durand, Arnaud and Lautemann, Clemens and More, Malika},
  title =	{{Counting Results in Weak Formalisms}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6451},
  editor =	{Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06451.4},
  URN =		{urn:nbn:de:0030-drops-9767},
  doi =		{10.4230/DagSemProc.06451.4},
  annote =	{Keywords: Small complexity classes, logic, polylog counting}
}
Document
Some Algebraic Problems with Connections to Circuit Complexity of Dynamic Data Structures

Authors: William Hesse

Published in: Dagstuhl Seminar Proceedings, Volume 6451, Circuits, Logic, and Games (2007)


Abstract
While researching dynamic data structures of polynomial size that are updated by extremely simple circuits, we have come across many interesting algebraic problems. Some of these simple questions about small sums and products in an algebra would give lower bounds on the complexity of dynamic data structures.

Cite as

William Hesse. Some Algebraic Problems with Connections to Circuit Complexity of Dynamic Data Structures. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 6451, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{hesse:DagSemProc.06451.5,
  author =	{Hesse, William},
  title =	{{Some Algebraic Problems with Connections to Circuit Complexity of Dynamic Data Structures}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6451},
  editor =	{Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06451.5},
  URN =		{urn:nbn:de:0030-drops-9749},
  doi =		{10.4230/DagSemProc.06451.5},
  annote =	{Keywords: Boolean Functions, auxiliary data, circuit complexity, lower bounds}
}
Document
Structure Theorem and Strict Alternation Hierarchy for FO² on Words

Authors: Philipp Weis and Neil Immerman

Published in: Dagstuhl Seminar Proceedings, Volume 6451, Circuits, Logic, and Games (2007)


Abstract
It is well-known that every first-order property on words is expressible using at most three variables. The subclass of properties expressible with only two variables is also quite interesting and well-studied. We prove precise structure theorems that characterize the exact expressive power of first-order logic with two variables on words. Our results apply to FO$^2[<]$ and FO$^2[<,suc]$, the latter of which includes the binary successor relation in addition to the linear ordering on string positions. For both languages, our structure theorems show exactly what is expressible using a given quantifier depth, $n$, and using $m$ blocks of alternating quantifiers, for any $mleq n$. Using these characterizations, we prove, among other results, that there is a strict hierarchy of alternating quantifiers for both languages. The question whether there was such a hierarchy had been completely open since it was asked in [Etessami, Vardi, and Wilke 1997].

Cite as

Philipp Weis and Neil Immerman. Structure Theorem and Strict Alternation Hierarchy for FO² on Words. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 6451, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{weis_et_al:DagSemProc.06451.6,
  author =	{Weis, Philipp and Immerman, Neil},
  title =	{{Structure Theorem and Strict Alternation Hierarchy for FO\~{A}‚\^{A}² on Words}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--22},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6451},
  editor =	{Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06451.6},
  URN =		{urn:nbn:de:0030-drops-9751},
  doi =		{10.4230/DagSemProc.06451.6},
  annote =	{Keywords: Descriptive complexity, finite model theory, alternation hierarchy, Ehrenfeucht-Fraisse games}
}
  • Refine by Author
  • 7 Vollmer, Heribert
  • 4 Schwentick, Thomas
  • 4 Thérien, Denis
  • 2 Beyersdorff, Olaf
  • 2 Meier, Arne
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 3 Boolean circuits
  • 3 Computational complexity theory
  • 3 finite model theory
  • 2 Proof complexity
  • 2 computational complexity
  • Show More...

  • Refine by Type
  • 12 document

  • Refine by Publication Year
  • 6 2007
  • 6 2010

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