Computer Science Logic: 21st International Workshop, Csl 2007, 16th Annual Conference Of The Eacsl, Lausanne, Switzerland, September 11-15, 2007 : Proceedings Csl 2007

This book constitutes the refereed proceedings of the 21st International Workshop on Computer Science Logic, CSL 2007, held as the 16th Annual Conference of the EACSL in Lausanne, Switzerland in September 2007. The 36 revised full papers presented together with the abstracts of six invited lectures were carefully reviewed and selected from 116 submissions. The papers are organized in topical sections on logic and games, expressiveness, games and trees, logic and deduction, lambda calculus, finite model theory, linear logic, proof theory, and game semantics. Front Matter....Pages - Full Completeness: Interactive and Geometric Characterizations of the Space of Proofs (Abstract)....Pages 1-2 The Symbolic Approach to Repeated Games (Abstract)....Pages 3-3 Proofs, Programs and Abstract Complexity....Pages 4-5 Model-Checking First-Order Logic: Automata and Locality....Pages 6-6 Tightening the Exchange Rates Between Automata....Pages 7-22 Precise Relational Invariants Through Strategy Iteration....Pages 23-40 Omega-Regular Half-Positional Winning Conditions....Pages 41-53 Clique-Width and Parity Games....Pages 54-68 Logical Refinements of Church’s Problem....Pages 69-83 The Power of Counting Logics on Restricted Classes of Finite Structures....Pages 84-98 Comparing the Expressive Power of Well-Structured Transition Systems....Pages 99-114 There Exist Some ω -Powers of Any Borel Rank....Pages 115-129 Satisfiability of a Spatial Logic with Tree Variables....Pages 130-145 Forest Expressions....Pages 146-160 MSO on the Infinite Binary Tree: Choice and Order....Pages 161-176 Classical and Intuitionistic Logic Are Asymptotically Identical....Pages 177-193 Qualitative Temporal and Spatial Reasoning Revisited....Pages 194-207 On Acyclic Conjunctive Queries and Constant Delay Enumeration....Pages 208-222 Integrating Linear Arithmetic into Superposition Calculus....Pages 223-237 The Theory of Calculi with Explicit Substitutions Revisited....Pages 238-252 A Soft Type Assignment System for λ -Calculus....Pages 253-267 Lambda Theories of Effective Lambda Models....Pages 268-282 Typed Normal Form Bisimulation....Pages 283-297 Not Enough Points Is Enough....Pages 298-312 Classical Program Extraction in the Calculus of Constructions....Pages 313-327 Building Decision Procedures in the Calculus of Inductive Constructions....Pages 328-342 Structure Theorem and Strict Alternation Hierarchy for FO 2 on Words....Pages 343-357 On the Complexity of Reasoning About Dynamic Policies....Pages 358-373 Relativizing Small Complexity Classes and Their Theories....Pages 374-388 Subexponential Time and Fixed-Parameter Tractability: Exploiting the Miniaturization Mapping....Pages 389-404 From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic....Pages 405-419 Linear Realizability....Pages 420-434 Correctness of Multiplicative (and Exponential) Proof Structures is NL -Complete....Pages 435-450 Focusing and Polarization in Intuitionistic Logic....Pages 451-465 Incorporating Tables into Proofs....Pages 466-480 A Cut-Free and Invariant-Free Sequent Calculus for PLTL ....Pages 481-495 Unbounded Proof-Length Speed-Up in Deduction Modulo....Pages 496-511 Propositional Logic for Circuit Classes....Pages 512-526 Game Characterizations and the PSPACE-Completeness of Tree Resolution Space....Pages 527-541 Continuous Previsions....Pages 542-557 Bad Variables Under Control....Pages 558-572 A Games Model of Bunched Implications....Pages 573-588 The Ackermann Award 2007....Pages 589-597 Back Matter....Pages - This book constitutes the refereed proceedings of the 21st International Workshop on Computer Science Logic, CSL 2007, held as the 16th Annual Conference of the EACSL in Lausanne, Switzerland, in September 2007. The 36 revised full papers presented together with the abstracts of 6 invited lectures were carefully reviewed and selected from 116 submissions. The papers are organized in topical sections on logic and games, expressiveness, games and trees, logic and deduction, lambda calculus, finite model theory, linear logic, proof theory, and game semantics Invited Lectures -- Logic And Games -- Expressiveness -- Games And Trees -- Logic And Deduction -- Lambda Calulus -- Finite Model Theory -- Linear Logic -- Proof Theory -- Game Semantics. Jacques Duparc, Thomas A. Henzinger (eds.). Includes Bibliographical References And Index. Also Issued Online.