Computer Science Logic: 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings (Lecture Notes in Computer Science, 3634)

This book constitutes the refereed proceedings of the 19th International Workshop on Computer Science Logic, CSL 2005, held as the 14th Annual Conference of the EACSL in Oxford, UK in August 2005. The 33 revised full papers presented together with 4 invited contributions were carefully reviewed and selected from 108 papers submitted. All current aspects of logic in computer science are addressed ranging from mathematical logic and logical foundations to methodological issues and applications of logics in various computing contexts. The volume is organized in topical sections on semantics and logics, type theory and lambda calculus, linear logic and ludics, constraints, finite models, decidability and complexity, verification and model checking, constructive reasoning and computational mathematics, and implicit computational complexity and rewriting. Xml Navigation And Tarski's Relation Algebras / Maarten Marx -- Verification In Predicate Logic With Time : Algorithmic Questions / Anatol Slissenko -- Note On Formal Analogical Reasoning In The Juridical Context / Matthias Baaz -- An Abstract Strong Normalization Theorem / Ulrich Berger -- On Bunched Polymorphism / Matthew Collinson, David Pym And Edmund Robinson -- Distributed Control Flow With Classical Modal Logic / Tom Murphy Vii, Karl Crary And Robert Harper -- A Logic Of Coequations / Jiri Adamek -- A Semantic Formulation Of Tt-lifting And Logical Predicates For Computational Metalanguage / Shin-ya Katsumata -- Order Structures On Bohm-like Models / Paula Severi And Fer-jan De Vries -- Higher-order Matching And Games / Colin Stirling -- Decidability Of Type-checking In The Calculus Of Algebraic Constructions With Size Annotations / Frederic Blanqui -- On The Role Of Type Decorations In The Calculus Of Inductive Constructions / Bruno Barras And Benjamin Gregoire -- L-nets, Strategies And Proof-nets / Pierre-louis Curien And Claudia Faggian -- Permutative Logic / Jean-marc Andreoli, Gabriele Pulcini And Paul Ruet -- Focusing The Inverse Method For Linear Logic / Kaustuv Chaudhuri And Frank Pfenning -- Towards A Typed Geometry Of Interaction / Esfandiar Haghverdi And Philip J. Scott -- From Pebble Games To Tractability : An Ambidextrous Consistency Algorithm For Quantified Constraint Satisfaction / Hubie Chen And Victor Dalmau -- An Algebraic Approach For The Unsatisfiability Of Nonlinear Constraints / Ashish Tiwari -- Coprimality In Finite Models / Marcin Mostowski And Konrad Zdanowski -- Towards A Characterization Of Order-invariant Queries Over Tame Structures / Michael Benedikt And Luc Segoufin -- Decidability Of Term Algebras Extending Partial Algebras / Bakhadyr Khoussainov And Sasha Rubin -- Results On The Guarded Fragment With Equivalence Or Transitive Relations / Emanuel Kieronski -- The Modular Decomposition Of Countable Graphs : Constructions In Monadic Second-order Logic / Bruno Courcelle And Christian Delhomme -- On The Complexity Of Hybrid Logics With Binders / Balder Ten Cate And Massimo Franceschet -- The Complexity Of Independence-friendly Fixpoint Logic / Julian Bradfield And Stephan Kreutzer -- Closure Properties Of Weak Systems Of Bounded Arithmetic / Antonina Kolokolova -- Transfinite Extension Of The Mu-calculus / Julian Bradfield, Jacques Duparc And Sandra Quickert -- Bounded Model Checking Of Pointer Programs / Witold Charatonik, Lilia Georgieva And Patrick Maier -- Pdl With Intersection And Converse Is Decidable / Carsten Lutz -- On Deciding Topological Classes Of Deterministic Tree Languages / Filip Murak -- Complexity And Intensionality In A Type-1 Framework For Computable Analysis / Branimir Lambov -- Computing With Sequences, Weak Topologies And The Axiom Of Choice / Vasco Brattka And Matthias Schroder -- Light Functional Interpretation / Mircea-dan Hernest -- Feasible Proofs Of Matrix Properties With Csanky's Algorithm / Michael Soltys -- A Propositional Proof System For Log Space / Steven Perron -- Identifying Polynomial-time Recursive Functions / Carsten Schurmann And Jatin Shah -- Confluence Of Shallow Right-linear Rewrite Systems / Guillem Godoy And Ashish Tiwari -- App. The Ackermann Award 2005 / Erich Gradel, Janos Makowsky And Alexander Razborov -- App. Clemens Lauteman : 1951-2005 An Obituary. Luke Ong (ed.). Includes Bibliographical References And Index. Also Issued Online. Front Matter....Pages - XML Navigation and Tarski’s Relation Algebras....Pages 1-2 Verification in Predicate Logic with Time: Algorithmic Questions....Pages 3-17 Note on Formal Analogical Reasoning in the Juridical Context....Pages 18-26 An Abstract Strong Normalization Theorem....Pages 27-35 On Bunched Polymorphism....Pages 36-50 Distributed Control Flow with Classical Modal Logic....Pages 51-69 A Logic of Coequations....Pages 70-86 A Semantic Formulation of ⊤ ⊤-Lifting and Logical Predicates for Computational Metalanguage....Pages 87-102 Order Structures on Böhm-Like Models....Pages 103-118 Higher-Order Matching and Games....Pages 119-134 Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations....Pages 135-150 On the Role of Type Decorations in the Calculus of Inductive Constructions....Pages 151-166 L-Nets, Strategies and Proof-Nets....Pages 167-183 Permutative Logic....Pages 184-199 Focusing the Inverse Method for Linear Logic....Pages 200-215 Towards a Typed Geometry of Interaction....Pages 216-231 From Pebble Games to Tractability: An Ambidextrous Consistency Algorithm for Quantified Constraint Satisfaction....Pages 232-247 An Algebraic Approach for the Unsatisfiability of Nonlinear Constraints....Pages 248-262 Coprimality in Finite Models....Pages 263-275 Towards a Characterization of Order-Invariant Queries over Tame Structures....Pages 276-291 Decidability of Term Algebras Extending Partial Algebras....Pages 292-308 Results on the Guarded Fragment with Equivalence or Transitive Relations....Pages 309-324 The Modular Decomposition of Countable Graphs: Constructions in Monadic Second-Order Logic....Pages 325-338 On the Complexity of Hybrid Logics with Binders....Pages 339-354 The Complexity of Independence-Friendly Fixpoint Logic....Pages 355-368 Closure Properties of Weak Systems of Bounded Arithmetic....Pages 369-383 Transfinite Extension of the Mu-Calculus....Pages 384-396 Bounded Model Checking of Pointer Programs....Pages 397-412 PDL with Intersection and Converse Is Decidable....Pages 413-427 On Deciding Topological Classes of Deterministic Tree Languages....Pages 428-441 Complexity and Intensionality in a Type-1 Framework for Computable Analysis....Pages 442-461 Computing with Sequences, Weak Topologies and the Axiom of Choice....Pages 462-476 Light Functional Interpretation....Pages 477-492 Feasible Proofs of Matrix Properties with Csanky’s Algorithm....Pages 493-508 A Propositional Proof System for Log Space....Pages 509-524 Identifying Polynomial-Time Recursive Functions....Pages 525-540 Confluence of Shallow Right-Linear Rewrite Systems....Pages 541-556 The Ackermann Award 2005....Pages 557-565 Clemens Lautemann: 1951-2005 An Obituary ....Pages 566-566 Back Matter....Pages - "The Annual Conference of the European Association for Computer Science Logic (EACSL), CSL 2005, was held at the University of Oxford on 22 -25 August 2005."