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

Jacques Duparc, Thomas A. Henzinger9783540749141, 3540749144

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.

---

Table of contents :
1……Page 1
Introduction……Page 12
The Symbolic Approach to Repeated Games……Page 14
Proofs, Programs and Abstract Complexity……Page 15
Model-Checking First-Order Logic: Automata and Locality……Page 17
Introduction……Page 18
Preliminaries……Page 20
Safety Properties and Their Verification……Page 21
Fine Automata and Their Construction……Page 23
From Büchi to co-Büchi Automata……Page 25
From Büchi to Limit Finite Automata……Page 28
Discussion……Page 30
Introduction……Page 34
Systems of Rational Equations……Page 36
Least Solutions of Systems of Rational Equations……Page 38
Systems of Conjunctive Equations……Page 40
Analyzing Affine Programs……Page 44
Systems of Rational Equations with LP……Page 48
Conclusion……Page 50
Introduction……Page 52
Preliminaries……Page 53
Types of Arenas……Page 55
Simplifying the Witness Arena……Page 56
Decidability……Page 58
Examples of $omega$-Regular Half-Positional Winning Conditions……Page 59
Conclusion and Future Work……Page 62
Introduction……Page 65
Parity Games……Page 67
Joint Choice Property……Page 68
Clique Width……Page 69
Algorithm……Page 72
Algorithms for Operators……Page 74
Dropping the Restriction on Colours……Page 77
Introduction……Page 80
Church’s Problem, Games, and Strategies……Page 82
Fragments of MSO and Main Result……Page 83
On Definability of Causal Operators……Page 84
Muller and Parity Games and Their Weak Versions……Page 85
From (Weak) Muller to (Weak) Parity Conditions……Page 86
Types……Page 87
Strong Normal Forms……Page 88
Weak Normal Forms……Page 89
Logics with Strong or Weak Normal Form……Page 91
Proof of Theorem 2……Page 92
Discussion and Perspectives……Page 93
Introduction……Page 95
Background……Page 97
Tree-Width……Page 98
Graph Minors……Page 99
CFI Graphs……Page 100
Tree-Width……Page 101
Bounded Local Tree-Width……Page 105
Graph Minors……Page 106
Introduction……Page 110
Preliminaries on Well-Structured Transition Systems……Page 112
Constrained Multiset Rewriting Systems……Page 113
Lossy FIFO Channel Systems……Page 116
Petri Nets and Their Extensions……Page 120
(Integral) Relational Automata……Page 122
Conclusions……Page 124
Introduction……Page 126
Topology……Page 127
Main Result……Page 129
Concluding Remarks and Further Work……Page 138
Introduction……Page 141
Preliminaries……Page 143
The Tree Query Logic……Page 144
Definitions……Page 147
Configurations……Page 149
Adding Disequalities to Positive Bounded TAGED……Page 151
From TQL to Automata……Page 152
Extending MSO with Tree Isomorphism Tests……Page 154
Conclusion……Page 155
Introduction……Page 157
The Regular Expressions……Page 158
Forest Automata……Page 160
Equivalence with First-Order Logic……Page 161
Equivalence with Chain Logic……Page 163
Concatenation Hierarchy……Page 165
Introduction……Page 172
Preliminaries……Page 173
Choice……Page 174
Undefinability of Choice Functions……Page 175
Applications of the Result and Its Proof……Page 179
Well-Ordered Trees……Page 182
Interpreting $t_llex$……Page 183
Introduction……Page 188
Generating Functions……Page 190
Tautologies and Non-tautologies……Page 192
Simple Non-tautologies……Page 194
Simple Tautologies……Page 196
Less Simple Non-tautologies……Page 197
Pierce Formulas……Page 200
Final Remarks……Page 203
Introduction……Page 205
Preliminaries……Page 207
Consistency and QNUFs……Page 210
Posets……Page 213
The Point Algebra, Fragments, and Extensions……Page 214
Extensions……Page 215
Spatial Reasoning……Page 216
On Acyclic Conjunctive Queries and Constant Delay Enumeration……Page 219
Complexity Framework……Page 221
Logical Framework……Page 222
Acyclic Conjunctive Queries……Page 223
Quantifier Elimination……Page 225
Combinatorial Tools……Page 227
Enumeration of Quantifier-Free and Free-Connex Acyclic Queries……Page 228
A Dichotomy Result……Page 230
Free-Connex Treewidth……Page 232
Introduction……Page 234
Preliminaries……Page 235
The Calculus for Ground Clauses……Page 237
Lifting……Page 242
Finite-Based Ordering……Page 244
Negative Results……Page 245
Conclusions……Page 246
References……Page 247
Introduction……Page 249
Syntax……Page 252
Confluence on Metaterms……Page 254
The Confluence Proof……Page 255
Preservation of $beta$-Strong Normalisation……Page 256
The $lambda esw$-Calculus……Page 257
The $Lambda_I$-Calculus……Page 258
The Typed $lambda es$-Calculus……Page 259
Conclusion……Page 261
Introduction……Page 264
Soft Linear Logic and $lambda$-Calculus……Page 266
The Soft Type Assignment System……Page 267
Subject Reduction……Page 270
Complexity……Page 272
Complexity of Reductions in STA……Page 273
Polynomial Time Completeness……Page 275
Introduction……Page 279
Preliminaries……Page 281
Lambda Calculus and Lambda Models……Page 282
Graph Models……Page 283
Effective Lambda Models……Page 285
Can Effective $lambda$-Models Have an r.e. Theory?……Page 287
The Löwenheim-Skolem Theorem……Page 289
The Minimum Order Graph Theory……Page 291
Background……Page 294
Contributions……Page 295
Related Work……Page 296
Syntax and Semantics……Page 297
Normal Form Bisimulation……Page 299
Alternating Substitution……Page 301
Fixed Point Combinators Are Unique……Page 304
Syntactic Minimal Invariance……Page 305
References……Page 307
Introduction……Page 309
Cartesian Closed Categories……Page 311
The Untyped $lambda$-Calculus and Its Models……Page 312
Building a Syntactical $lambda$-Model……Page 313
A Cartesian Closed Category of Sets and Relations……Page 317
Interpreting the Untyped $lambda$-Calculus in $D$……Page 319
Conclusions and Further Works……Page 321
Modelling Non-determinism……Page 320
Classical Program Extraction in the Calculus of Constructions……Page 324
Typing……Page 326
Terms, Stacks and Processes……Page 327
Definition……Page 329
Cartesian Product of a Family of $pi$-Sets……Page 330
An Alternative Encoding of Functions……Page 331
The Interpretation Function……Page 332
Soundness……Page 333
Peirce’s Law and the Excluded Middle……Page 334
Decomposing the Propositional Dependent Product……Page 335
Adding a Primitive Type of Natural Numbers……Page 337
Introduction……Page 339
The Calculus……Page 342
Computation by Conversion……Page 343
Two Simple Examples……Page 346
Stability by Substitution……Page 347
Conversion as Rewriting……Page 348
Conclusion and Discussion……Page 350
Introduction……Page 354
Background and Definitions……Page 357
Structure Theorem for FO$^2$[