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