 |
 |
Special Issue for the Conference on Computer Science Logic CSL 2009
2009 Editor: Reinhard Kahle, Erich Grädel
1. From coinductive proofs to exact real arithmetic: theory and applications
Based on a new coinductive characterization of continuous functions we extract certified programs for exact real number computation from constructive proofs. The extracted programs construct and combine exact real number algorithms with respect to the binary signed digit representation of real numbers. The data type corresponding to the coinductive definition of continuous functions consists of finitely branching non-wellfounded trees describing when the algorithm writes and reads digits. We discuss several examples including the extraction of programs for polynomials up to degree two and the definite integral of continuous maps.
2. Functional Interpretations of Intuitionistic Linear Logic
We present three different functional interpretations of intuitionistic linear logic ILL and show how these correspond to well-known functional interpretations of intuitionistic logic IL via embeddings of IL into ILL. The main difference from previous work of the second author is that in intuitionistic linear logic (as opposed to classical linear logic) the interpretations of !A are simpler and simultaneous quantifiers are no longer needed for the characterisation of the interpretations. We then compare our approach in developing these three proof interpretations with the one of de Paiva around the Dialectica category model of linear logic.
3. EXPTIME Tableaux for the Coalgebraic mu-Calculus
The coalgebraic approach to modal logic provides a uniform framework that captures the semantics of a large class of structurally different modal logics, including e.g. graded and probabilistic modal logics and coalition logic. In this paper, we introduce the coalgebraic mu-calculus, an extension of the general (coalgebraic) framework with fixpoint operators. Our main results are completeness of the associated tableau calculus and EXPTIME decidability for guarded formulas. Technically, this is achieved by reducing satisfiability to the existence of non-wellfounded tableaux, which is in turn equivalent to the existence of winning strategies in parity games. Our results are parametric in the underlying class of models and yield, as concrete applications, previously unknown complexity bounds for the probabilistic mu-calculus and for an extension of coalition logic with fixpoints.
4. On the Parameterized Intractability of Monadic Second-Order Logic
One of Courcelle's celebrated results states that if C is a class of graphs of bounded tree-width, then model-checking for monadic second order logic (MSO_2) is fixed-parameter tractable (fpt) on C by linear time parameterized algorithms, where the parameter is the tree-width plus the size of the formula. An immediate question is whether this is best possible or whether the result can be extended to classes of unbounded tree-width. In this paper we show that in terms of tree-width, the theorem cannot be extended much further. More specifically, we show that if C is a class of graphs which is closed under colourings and satisfies certain constructibility conditions and is such that the tree-width of C is not bounded by \log^{84} n then MSO_2-model checking is not fpt unless SAT can be solved in sub-exponential time. If the tree-width of C is not poly-logarithmically bounded, then MSO_2-model checking is not fpt unless all problems in the polynomial-time hierarchy can be solved in sub-exponential time.
5. Tree-width for first order formulae
We introduce tree-width for first order formulae \phi, fotw(\phi). We show that computing fotw is fixed-parameter tractable with parameter fotw. Moreover, we show that on classes of formulae of bounded fotw, model checking is fixed parameter tractable, with parameter the length of the formula. This is done by translating a formula \phi\ with fotw(\phi)<k into a formula of the k-variable fragment L^k of first order logic. For fixed k, the question whether a given first order formula is equivalent to an L^k formula is undecidable. In contrast, the classes of first order formulae with bounded fotw are fragments of first order logic for which the equivalence is decidable. Our notion of tree-width generalises tree-width of conjunctive queries to arbitrary formulae of first order logic by taking into account the quantifier interaction in a formula. Moreover, it is more powerful than the notion of elimination-width of quantified constraint formulae, defined by Chen and Dalmau (CSL 2005): for quantified constraint formulae, both bounded elimination-width and bounded fotw allow for model checking in polynomial time. We prove that fotw of a quantified constraint formula \phi\ is bounded by the elimination-width of \phi, and we exhibit a class of quantified constraint formulae with bounded fotw, that has unbounded elimination-width. A similar comparison holds for strict tree-width of non-recursive stratified datalog as defined by Flum, Frick, and Grohe (JACM 49, 2002). Finally, […]
6. Pebble Games, Proof Complexity, and Time-Space Trade-offs
Pebble games were extensively studied in the 1970s and 1980s in a number of different contexts. The last decade has seen a revival of interest in pebble games coming from the field of proof complexity. Pebbling has proven to be a useful tool for studying resolution-based proof systems when comparing the strength of different subsystems, showing bounds on proof space, and establishing size-space trade-offs. This is a survey of research in proof complexity drawing on results and tools from pebbling, with a focus on proof space lower bounds and trade-offs between proof size and proof space.