Author name cluster

Michael Thomas 0001

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

1 author row

MFCS Conference 2011 Conference Paper

Verifying Proofs in Constant Depth

Olaf Beyersdorff
Samir Datta
Meena Mahajan
Gido Scharfenberger-Fabian
Karteek Sreenivasaiah
Michael Thomas 0001
Heribert Vollmer

Abstract In this paper we initiate the study of proof systems where verification of proofs proceeds by \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) circuits. We investigate the question which languages admit proof systems in this very restricted model. Formulated alternatively, we ask which languages can be enumerated by \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) functions. Our results show that the answer to this problem is not determined by the complexity of the language. On the one hand, we construct \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) proof systems for a variety of languages ranging from regular to \(\protect{\ensuremath{\mathsf{NP}}}\) -complete. On the other hand, we show by combinatorial methods that even easy regular languages such as Exact-OR do not admit \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) proof systems. We also present a general construction of \(\protect{\ensuremath{\mathsf{NC}}}^{0}\) proof systems for regular languages with strongly connected NFA’s.

Details

MFCS Conference 2010 Conference Paper

Counting Classes and the Fine Structure between NC 1 and L

Samir Datta
Meena Mahajan
B. V. Raghavendra Rao
Michael Thomas 0001
Heribert Vollmer

Abstract The class NC 1 of problems solvable by bounded fan-in circuit families of logarithmic depth is known to be contained in logarithmic space L, but not much about the converse is known. In this paper we examine the structure of classes in between NC 1 and L based on counting functions or, equivalently, based on arithmetic circuits. The classes PNC 1 and C = NC 1, defined by a test for positivity and a test for zero, respectively, of arithmetic circuit families of logarithmic depth, sit in this complexity interval. We study the landscape of Boolean hierarchies, constant-depth oracle hierarchies, and logarithmic-depth oracle hierarchies over PNC 1 and C = NC 1. We provide complete problems, obtain the upper bound L for all these hierarchies, and prove partial hierarchy collapses—in particular, the constant-depth oracle hierarchy over PNC 1 collapses to its first level PNC 1, and the constant-depth oracle hierarchy over C = NC 1 collapses to its second level.

Details

SAT Conference 2010 Conference Paper

Proof Complexity of Propositional Default Logic

Olaf Beyersdorff
Arne Meier
Sebastian Müller 0003
Michael Thomas 0001
Heribert Vollmer

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.

Details

JELIA Conference 2010 Conference Paper

Sets of Boolean Connectives That Make Argumentation Easier

Nadia Creignou
Johannes Schmidt 0001
Michael Thomas 0001
Stefan Woltran

Abstract Many proposals for logic-based formalizations of argumentation consider an argument as a pair (Φ, α ), where the support Φ is understood as a minimal consistent subset of a given knowledge base which has to entail the claim α. In most scenarios, arguments are given in the full language of classical propositional logic which makes reasoning in such frameworks a computationally costly task. For instance, the problem of deciding whether there exists a support for a given claim has been shown to be \(\Sigma^\mathrm{p}_2\) -complete. In order to better understand the sources of complexity (and to identify tractable fragments), we focus on arguments given over formulae in which the allowed connectives are taken from certain sets of Boolean functions. We provide a complexity classification for four different decision problems (existence of a support, checking the validity of an argument, relevance and dispensability) with respect to all possible sets of Boolean functions.

Details

TIME Conference 2009 Conference Paper

Model Checking CTL is Almost Always Inherently Sequential

Olaf Beyersdorff
Arne Meier
Michael Thomas 0001
Heribert Vollmer
Martin Mundhenk
Thomas Schneider 0002

The model checking problem for CTL is known to be P-complete (Clarke, Emerson, and Sistla (1986), see Schnoebelen (2002)). We consider fragments of CTL obtained by restricting the use of temporal modalities or the use of negations---restrictions already studied for LTL by Sistla and Clarke (1985) and Markey (2004). For all these fragments, except for the trivial case without any temporal operator, we systematically prove model checking to be either inherently sequential (P-complete) or very efficiently parallelizable (LOGCFL-complete). For most fragments, however, model checking for CTL is already P-complete. Hence our results indicate that in most applications, approaching CTL model checking by parallelism will not result in the desired speed up. We also completely determine the complexity of the model checking problem for all fragments of the extensions ECTL, CTL+, and ECTL+.

Details

SAT Conference 2009 Conference Paper

The Complexity of Reasoning for Fragments of Default Logic

Olaf Beyersdorff
Arne Meier
Michael Thomas 0001
Heribert Vollmer

Abstract Default logic was introduced by Reiter in 1980. In 1992, Gottlob classified the complexity of the extension existence problem for propositional default logic as \(\Sigma^{\rm P}_2\) -complete, and the complexity of the credulous and skeptical reasoning problem as \(\Sigma^{\rm P}_2\) -complete, resp. \(\Pi^{\rm P}_2\) -complete. Additionally, he investigated restrictions on the default rules, i. e. , semi-normal default rules. Selman made in 1992 a similar approach with disjunction-free and unary default rules. In this paper we systematically restrict the set of allowed propositional connectives. We give a complete complexity classification for all sets of Boolean functions in the meaning of Post’s lattice for all three common decision problems for propositional default logic. We show that the complexity is a trichotomy ( \(\Sigma^{\rm P}_2\) -, NP-complete, trivial) for the extension existence problem, whereas for the credulous and sceptical reasoning problem we get a finer classification down to NL-complete cases.

Details

MFCS Conference 2009 Conference Paper

The Complexity of Satisfiability for Fragments of Hybrid Logic-Part I

Arne Meier
Martin Mundhenk
Thomas Schneider 0002
Michael Thomas 0001
Volker Weber
Felix Weiss

Abstract The satisfiability problem of hybrid logics with the downarrow binder is known to be undecidable. This initiated a research program on decidable and tractable fragments. In this paper, we investigate the effect of restricting the propositional part of the language on decidability and on the complexity of the satisfiability problem over arbitrary, transitive, total frames, and frames based on equivalence relations. We also consider different sets of modal and hybrid operators. We trace the border of decidability and give the precise complexity of most fragments, in particular for all fragments including negation. For the monotone fragments, we are able to distinguish the easy from the hard cases, depending on the allowed set of operators.

Details

CSL Conference 2008 Conference Paper

Extensional Uniformity for Boolean Circuits

Pierre McKenzie
Michael Thomas 0001
Heribert Vollmer

Abstract Imposing an extensional uniformity condition on a non-uniform circuit complexity class \(\mathcal{C}\) means simply intersecting \(\mathcal{C}\) with a uniform class \(\mathcal{L}\). By contrast, the usual intensional uniformity conditions require that a resource-bounded machine be able to exhibit the circuits in the circuit family defining \(\mathcal{C}\). We say that \((\mathcal{C}, \mathcal{L})\) has the Uniformity Duality Property if the extensionally uniform class \(\mathcal{C}\cap\mathcal{L}\) can be captured intensionally by means of adding so-called \(\mathcal{L}\) -numerical predicates to the first-order descriptive complexity apparatus describing the connection language of the circuit family defining \(\mathcal{C}\). This paper exhibits positive instances and negative instances of the Uniformity Duality Property.

Details