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.
Author(s): Jacques Duparc, Thomas A. Henzinger
Edition: 1
Publisher: Springer
Year: 2007
Language: English
Pages: 610
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$[<]......Page 358
Alternation Hierarchy for FO$^2$[<]......Page 363
Structure Theorem and Alternation Hierarchy for FO$^2$[<, Suc]......Page 364
Small Models and Satisfiability for FO$^2$[<]......Page 366
Conclusion......Page 367
References......Page 368
Introduction......Page 369
DLP$_{\mathrm{dyn}^+$ and Its Fragments DLP$_{\mathrm{dyn}}$ and DLP......Page 371
PDL and Its Compressed Variants PDL$\oplus$ and PDL$\oplus$ [\mathbb{A}]......Page 373
Known Results and Difficulties of Reasoning About DLP$_{\mathrm{dyn}^+$ and Related Logics......Page 374
A Translation from DLP$_{\mathrm{dyn}^+$ to PDL$\oplus$ [\mathbb{A}]......Page 375
Satisfiability for PDL$\oplus$ [\mathbb{A}]......Page 378
2 EXP -Completeness of PDL$\oplus$......Page 381
Introduction......Page 385
Relativized Circuit Classes......Page 387
Relativized Logspace Classes......Page 388
Two-Sorted Languages and Complexity Classes......Page 389
Nonrelativized Theories......Page 392
Relativized Theories......Page 394
Separation Results......Page 396
Introduction......Page 400
Parameterized Complexity......Page 403
First-Order Logic......Page 404
An Example......Page 405
The General Framework......Page 406
Further Applications......Page 407
Fagin-Definable Problems......Page 409
Model-Checking Problems......Page 412
Conclusions......Page 414
Introduction......Page 416
Linear Logic Preliminaries......Page 417
Permutation of Rules in LL......Page 419
Focalization Graph......Page 420
Pre-focalization Process......Page 423
Dealing with Bias Assignments......Page 424
Quantifiers......Page 425
Exponentials......Page 426
Multi-focalization......Page 428
Conclusion and Future Works......Page 429
Introduction......Page 431
Combinatory Algebras......Page 432
Applicative Morphisms......Page 433
Categorical Models of Intuitionistic Linear Logic......Page 434
Assemblies and Modest Sets Realized by BCI Algebras......Page 435
Relational Linear Combinatory Algebras......Page 436
Assemblies and Modest Sets Realized by $rLCA's$......Page 439
Natural Number Object in Ass(A)......Page 440
Linear Lambda Calculus......Page 441
BCK Algebra with a Structure of $omega$-cppo......Page 442
Kleene's Second Algebra K_2......Page 443
Concluding remarks......Page 444
Correctness of Multiplicative (and Exponential) Proof Structures is NL-Complete......Page 446
MLL and Proof Structures......Page 447
MELL and Proof Structures......Page 449
Intuitionistic Multiplicative Linear Logic and Essential Nets......Page 451
Complexity Classes and Related Problems......Page 452
New Correctness Criteria for MLL and MELL......Page 454
NL-Completeness of the Criteria for MLL and MELL......Page 456
NL-Completeness of the Criterion for IMLL......Page 458
Conclusion and Acknowledgments......Page 460
About Focusing......Page 462
Methodology and Related Work......Page 463
Focusing in Linear Logic......Page 465
Translating Intuitionistic Logic......Page 466
Permeable Formulas and Their Polarity......Page 468
The $LJF$ Sequent Calculus......Page 469
Embedding Intuitionistic Systems in LJF......Page 472
Embedding Classical Logic in LJF......Page 473
Conclusion and Future Work......Page 475
Introduction......Page 477
Two Motivating Examples......Page 478
Tables as Multicut Derivations......Page 480
Focusing and Polarities......Page 481
Tables of Finite Successes......Page 483
Tables of Finite Failures......Page 485
Table as Proof Objects......Page 488
Conclusions and Future Work......Page 490
Introduction......Page 492
PLTL: Language and Model Theory......Page 493
The Sequent Calculus FC......Page 494
Derived Rules and Proofs......Page 496
Saturated Sets of Formulas......Page 499
Nondeterministic Models of FC-Consistent Sets......Page 501
Concluding Remarks......Page 505
Introduction......Page 507
Schematic Systems......Page 510
$i$-th Order Arithmetic......Page 511
Rewriting Formulæ......Page 512
Natural Deduction Modulo......Page 513
From $Z_i \lvdash[\textup{\textsf{N}}$ to $Z_i \lvdash[\textup{\textsf{S}}\$......Page 514
From $Z_i+1 \lvdash[\textup{\textsf{S}}$ and $Z_i+1 \lvdash[\textup{\textsf{N}}\$ to $Z_i \lvdash[\textup{\textsf{N}}\$_{R_i}......Page 516
Speed-Up Due to Computation......Page 518
Conclusion and Perspectives......Page 519
Introduction and Related Work......Page 523
Quantified Propositional Logic and Definition of the Calculus......Page 525
On Evaluating Circuits......Page 529
Sequential Iteration in Quantified Propositional Logic......Page 530
Circuit Evaluation and Iteration......Page 535
Introduction and Motivation......Page 538
Resolution Space......Page 539
Pebbling Contradictions......Page 540
Space and Games......Page 541
An Easy Case of the Pebbling Game......Page 542
Prover Strategy for the G_I DAGs......Page 543
Prover Strategy for the Lingas Circuits......Page 544
Delayer Strategy for Monotone Circuits......Page 548
PSPACE-Completeness of TCSP and P/D Game......Page 550
Introduction......Page 553
Preliminaries......Page 554
Continuous Games, Convexity, Concavity......Page 555
Continuous Previsions......Page 558
Hearts and Skins: Completeness......Page 563
Introduction......Page 569
IA, IA_catch......Page 571
Games......Page 572
The Essence of mkvar......Page 575
Proof of Full Abstraction......Page 577
Innocent Strategies Without mkvar......Page 578
Knowingness Without mkvar......Page 579
On Conservativity......Page 581
Introduction......Page 584
Bunched Implications and the $\alpha lambda$-Calculus......Page 585
Arenas......Page 587
Composition of Strategies......Page 588
Full Completeness for the $lambda$-Calculus......Page 590
Refining the Model......Page 591
Interpreting the $\alpha lambda$-Calculus......Page 596
Definability......Page 597
The Ackermann Award 2007......Page 600
45......Page 609
