Computer Science Logic: 21 International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings (Lecture Notes in Computer Science, 4646)

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. The 36 revised full papers presented together with the abstracts of six invited lectures 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. Title Page Preface Organization Table of Contents Full Completeness: Interactive and Geometric Characterizations of the Space of Proofs (Abstract) Introduction References The Symbolic Approach to Repeated Games (Abstract) Proofs, Programs and Abstract Complexity References Model-Checking First-Order Logic: Automata and Locality References Tightening the Exchange Rates Between Automata Introduction Preliminaries Translating Safety Properties to Automata Safety Properties and Their Verification Fine Automata and Their Construction Discussion FromB$\'' {u}$chi to co-B$\'' {u}$chi Automata From B$\'' {u}$chi to Limit Finite Automata Discussion References Precise Relational Invariants Through Strategy Iteration Introduction Systems of Rational Equations Least Solutions of Systems of Rational Equations Systems of Conjunctive Equations The Result Analyzing Affine Programs Systems of Rational Equations with LP Conclusion References Omega-Regular Half-Positional Winning Conditions Introduction Preliminaries Types of Arenas Simplifying the Witness Arena Decidability Examples of ω-Regular Half-Positional Winning Conditions Conclusion and Future Work References Clique-Width and Parity Games Introduction Parity Games Joint Choice Property Clique Width $k$-Expressions and $t$-Strategies Algorithm Algorithms for Operators Complexity Dropping the Restriction on Colours References Logical Refinements of Church’s Problem Introduction Preliminaries and Main Result Church’s Problem, Games, and Strategies Fragments of MSO and Main Result On Definability of Causal Operators Preliminaries on Games and Automata Muller and Parity Games and Their Weak Versions From (Weak) Muller to (Weak) Parity Conditions Normal Forms Types Strong Normal Forms Weak Normal Forms Proof of Theorems 1 and 2 Logics with Strong or Weak Normal Form Strictly Bounded Logic Proof of Theorem 2 Discussion and Perspectives References The Power of Counting Logics on Restricted Classes of Finite Structures Introduction Background Counting Logics Tree-Width Graph Minors CFI Graphs Tree-Width Bounded Local Tree-Width Graph Minors References Comparing the Expressive Power of Well-Structured Transition Systems Introduction Preliminaries on Well-Structured Transition Systems Constrained Multiset Rewriting Systems Lossy FIFO Channel Systems Petri Nets and Their Extensions (Integral) Relational Automata Conclusions References There Exist Some $\omega$ -Powers of Any Borel Rank Introduction Topology MainResult Concluding Remarks and Further Work References Satisfiability of a Spatial Logic with Tree Variables Introduction Preliminaries The Tree Query Logic Tree Automata with Global Equalities and Disequalities Definitions Configurations Adding Disequalities to Positive Bounded TAGED From TQL to Automata Extending MSO with Tree Isomorphism Tests Conclusion References Forest Expressions Introduction The Regular Expressions Comparison with Existing Expressions Forest Automata Equivalence with First-Order Logic Equivalence with Chain Logic Concatenation Hierarchy References MSO on the Infinite Binary Tree: Choice and Order Introduction Preliminaries Choice Undefinability of Choice Functions Applications of the Result and Its Proof Order Well-Ordered Trees Interpreting $t_{\textrm{llex}}$ References Classical and Intuitionistic Logic Are Asymptotically Identical Introduction Generating Functions Tautologies and Non-tautologies Enumeration of Classes Simple Non-tautologies Simple Tautologies Less Simple Non-tautologies Pierce Formulas FinalRemarks References Qualitative Temporal and Spatial Reasoning Revisited Introduction Preliminaries Consistency and QNUFs Posets The Point Algebra, Fragments, and Extensions Fragments Extensions Spatial Reasoning References On Acyclic Conjunctive Queries and Constant Delay Enumeration Preliminaries Problems Complexity Framework Logical Framework Hypergraphs Acyclic Conjunctive Queries Quantifier Elimination Covers and Representative Sets Quantifier Elimination Constant Delay Enumeration Combinatorial Tools Enumeration of Quantifier-Free and Free-Connex Acyclic Queries A Dichotomy Result Free-Connex Treewidth References Integrating Linear Arithmetic into Superposition Calculus Introduction Preliminaries The Calculus for Ground Clauses Lifting Finite-Based Ordering Negative Results Conclusions References The Theory of Calculi with Explicit Substitutions Revisited Introduction Syntax Confluence on Metaterms The Confluence Proof Preservation of $\beta$-Strong Normalisation The $\lesw$-Calculus The $\LI$-Calculus Solving the Puzzle The Typed $\les$-Calculus Conclusion References A Soft Type Assignment System for $\lambda$-Calculus Introduction Soft Linear Logic and $\lambda$-Calculus The Soft Type Assignment System Subject Reduction Complexity Complexity of Reductions in STA Polynomial Time Completeness References Lambda Theories of Effective Lambda Models Introduction Preliminaries Lambda Calculus and Lambda Models Effective Domains Graph Models Co-r.e. Sets of Lambda Terms EffectiveLambdaModels CanEffectiveλ-Models Have an r.e. Theory? TheL$\" {o}$wenheim-Skolem Theorem The Minimum Order Graph Theory References Typed Normal Form Bisimulation Introduction Background Contributions Related Work Jump-With-Argument Syntax and Semantics Ultimate Pattern Matching Normal Form Bisimulation Alternating Substitution Examples Fixed Point Combinators Are Unique Syntactic Minimal Invariance References Not Enough Points Is Enough Introduction Preliminaries Generalities Cartesian Closed Categories The Untyped $\lambda$-Calculus and Its Models From Reflexive Objects to $\lambda$-Models Building a Syntactical $\lambda$-Model Working Without Countable Products A Cartesian Closed Category of Sets and Relations An Extensional Relational Model of $\lambda$-Calculus Constructing an Extensional Reflexive Object Interpreting the Untyped $\lambda$-Calculus in $\mathcal {D}$ Modelling Non-determinism Conclusions and Further Works References Classical Program Extraction in the Calculus of Constructions A Proof-Irrelevant Calculus of Constructions Syntax Typing The Language of Realisers Terms, Stacks and Processes Evaluation and Realisability The $\prod$ -Set Structure Definition Cartesian Product of a Family of $\prod$-Sets Degenerated $\prod$-Sets Subtyping Constructing the Model An Alternative Encoding of Functions Interpreting Sorts The Interpretation Function Soundness Adequacy Extensions of the Formalism Peirce’s Law and the Excluded Middle Decomposing the Propositional Dependent Product Adding a Primitive Type of Natural Numbers References Building Decision Procedures in the Calculus of Inductive Constructions Introduction The Calculus Computation by Conversion Two Simple Examples Metatheorical Properties Stability by Substitution Conversion as Rewriting Decidability of Type Checking Conclusion and Discussion References Structure Theorem and Strict Alternation Hierarchy for FO^{2} on Words Introduction Background and De nitions Structure Theorem for FO^{2}[