Computer Science Logic: 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001 Proceedings (Lecture Notes in Computer Science (2142))

This book constitutes the refereed proceedings of the 15th International Workshop on Computer Science Logic, CSL 2001, held as the 10th Annual Conerence of the EACSL in Paris, France in September 2001. The 39 revised full papers presented together with two invited papers were carefully reviewed and selected from 91 submissions. The papers are organized in topical sections on linear logic, descriptive complexity, semantics, higher-order programs, model logics, verification, automata, lambda calculus, induction, equational calculus, and constructive theory of types. Local Reasoning about Programs that Alter Data Structures....Pages 1-19 Applications of Alfred Tarski’s Ideas in Database Theory....Pages 20-37 Locus Solum: From the Rules of Logic to the Logic of Rules....Pages 38-38 The Expressive Power of Horn Monadic Linear Logic....Pages 39-53 Non-commutativity and MELL in the Calculus of Structures....Pages 54-68 Quadratic Correctness Criterion for Non-commutative Logic....Pages 69-83 Capture Complexity by Partition....Pages 84-98 An Existential Locality Theorem....Pages 99-114 Actual Arithmetic and Feasibility....Pages 115-129 The Natural Order-Generic Collapse for ω -Representable Databases over the Rational and the Real Ordered Group....Pages 130-144 An Algebraic Foundation for Higraphs....Pages 145-159 Semantic Characterisations of Second-Order Computability over the Real Numbers....Pages 160-172 An Abstract Look at Realizability....Pages 173-187 The Anatomy of Innocence....Pages 188-202 An Improved Extensionality Criterion for Higher-Order Logic Programs....Pages 203-216 A Logic for Abstract State Machines....Pages 217-231 Constrained Hyper Tableaux....Pages 232-246 Modal Logic and the Two-Variable Fragment....Pages 247-261 A Logic for Approximate First-Order Reasoning....Pages 262-276 Inflationary Fixed Points in Modal Logic....Pages 277-291 Categorical and Kripke Semantics for Constructive S4 Modal Logic....Pages 292-307 Labelled Natural Deduction for Interval Logics....Pages 308-323 Decidable Navigation Logics for Object Structures....Pages 324-338 The Decidability of Model Checking Mobile Ambients....Pages 339-354 A Generalization of the Büchi-Elgot-Trakhtenbrot Theorem....Pages 355-368 An Effective Extension of the Wagner Hierarchy to Blind Counter Automata....Pages 369-383 Decision Procedure for an Extension of WS1S....Pages 384-398 Limiting Partial Combinatory Algebras towards Infinitary Lambda-Calculi and Classical Logic....Pages 399-414 Intersection Logic....Pages 414-429 Life without the Terminal Type....Pages 429-442 Fully Complete Minimal PER Models for the Simply Typed λ-Calculus....Pages 443-457 A Principle of Induction....Pages 458-468 On a Generalisation of Herbrand’s Theorem....Pages 469-483 Well-Founded Recursive Relations....Pages 484-498 Stratified Context Unification Is in PSPACE....Pages 498-513 Uniform Derivation of Decision Procedures by Superposition....Pages 513-527 Complete Categorical Equational Deduction....Pages 528-538 Beyond Regularity: Equational Tree Automata for Associative and Commutative Theories....Pages 539-553 Normalized Types....Pages 554-569 Markov’s Principle for Propositional Type Theory....Pages 570-584 Recursion for Higher-Order Encodings....Pages 585-599 Monotone Inductive and Coinductive Constructors of Rank 2....Pages 600-614 Computer Science Logic: 15th International Workshop, CSL 2001 10th Annual Conference of the EACSL Paris, France, September 10–13, 2001, Proceedings Author: Laurent Fribourg Published by Springer Berlin Heidelberg ISBN: 978-3-540-42554-0 DOI: 10.1007/3-540-44802-0 Table of Contents: Local Reasoning about Programs that Alter Data Structures Applications of Alfred Tarski’s Ideas in Database Theory Locus Solum: From the Rules of Logic to the Logic of Rules The Expressive Power of Horn Monadic Linear Logic Non-commutativity and MELL in the Calculus of Structures Quadratic Correctness Criterion for Non-commutative Logic Capture Complexity by Partition An Existential Locality Theorem Actual Arithmetic and Feasibility The Natural Order-Generic Collapse for ω-Representable Databases over the Rational and the Real Ordered Group An Algebraic Foundation for Higraphs Semantic Characterisations of Second-Order Computability over the Real Numbers An Abstract Look at Realizability The Anatomy of Innocence An Improved Extensionality Criterion for Higher-Order Logic Programs A Logic for Abstract State Machines Constrained Hyper Tableaux Modal Logic and the Two-Variable Fragment A Logic for Approximate First-Order Reasoning Inflationary Fixed Points in Modal Logic