Dagstuhl Seminar Proceedings, Volume 10061
Dagstuhl Seminar Proceedings
DagSemProc
https://www.dagstuhl.de/dagpub/1862-4405
https://dblp.org/db/series/dagstuhl
1862-4405
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
10061
2010
https://drops.dagstuhl.de/entities/volume/DagSemProc-volume-10061
10061 Abstracts Collection – Circuits, Logic, and Games
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.
Computational complexity theory
Finite model theory
Boolean circuits
Regular languages
Finite monoids
Ehrenfeucht-Fra{\''i}ssé-games
1-8
Regular Paper
Benjamin
Rossman
Benjamin Rossman
Thomas
Schwentick
Thomas Schwentick
Denis
Thérien
Denis Thérien
Heribert
Vollmer
Heribert Vollmer
10.4230/DagSemProc.10061.1
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
10061 Executive Summary – Circuits, Logic, and Games
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.
Computational complexity theory
finite model theory
Boolean circuits
regular languages
finite monoids
Ehrenfeucht-Fra\"\i ss\'e-games
1-5
Regular Paper
Benjamin
Rossman
Benjamin Rossman
Thomas
Schwentick
Thomas Schwentick
Denis
Thérien
Denis Thérien
Heribert
Vollmer
Heribert Vollmer
10.4230/DagSemProc.10061.2
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Complexity Results for Modal Dependence Logic
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.
Dependence logic
satisfiability problem
computational complexity
poor man's logic
1-15
Regular Paper
Peter
Lohmann
Peter Lohmann
Heribert
Vollmer
Heribert Vollmer
10.4230/DagSemProc.10061.3
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Hardness of Parameterized Resolution
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.
Proof complexity
parameterized complexity
Resolution
Prover-Delayer Games
1-28
Regular Paper
Olaf
Beyersdorff
Olaf Beyersdorff
Nicola
Galesi
Nicola Galesi
Massimo
Lauria
Massimo Lauria
10.4230/DagSemProc.10061.4
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Proof Complexity of Propositional Default Logic
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.
Proof complexity
default logic
sequent calculus
1-14
Regular Paper
Olaf
Beyersdorff
Olaf Beyersdorff
Arne
Meier
Arne Meier
Sebastian
Müller
Sebastian Müller
Michael
Thomas
Michael Thomas
Heribert
Vollmer
Heribert Vollmer
10.4230/DagSemProc.10061.5
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
The Complexity of Reasoning for Fragments of Autoepistemic Logic
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.
Autoepistemic logic
computational complexity
nonmonotonic reasoning
Post's lattice
1-10
Regular Paper
Nadia
Creignou
Nadia Creignou
Arne
Meier
Arne Meier
Michael
Thomas
Michael Thomas
Heribert
Vollmer
Heribert Vollmer
10.4230/DagSemProc.10061.6
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode