Logic, Language, Information and Computation: 14th International Workshop, WoLLIC 2007, Rio de Janeiro, Brazil, July 2-5, 2007, Proceedings (Lecture Notes in Computer Science, 4576)

Welcome to the proceedings of the 14th WoLLIC meeting, which was held in Rio de Janeiro, Brazil, July 2 - 5, 2007. The Workshop on Logic, Language, Information and Computation (WoLLIC) is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. The WoLLIC meetings alternate between Brazil (and Latin America) and other countries, with the aim of fostering interest in applied logic among Latin Am- ican scientists and students, and facilitating their interaction with the international - plied logic community. WoLLIC 2007 focused on foundationsof computing and programming,novel c- putation models and paradigms, broad notions of proof and belief, formal methods in software and hardware development; logical approaches to natural language and r- soning; logics of programs, actions and resources; foundational aspects of information organization, search, ?ow, sharing, and protection. The Program Committee for this meeting, consisting of the 28 colleagues listed here, was designed to promote these inter-disciplinary and cross-disciplinary topics. Like its predecessors, WoLLIC 2007 included invited talks and tutorials as well as contributed papers. The Program Committee received 52 complete submissions (aside from 15 preliminary abstracts which did not materialize). A thorough review process by the Program Committee, assisted by over 70 external reviewers, led to the acc- tance of 21 papers for presentation at the meeting and inclusion in these proceedings. The conference program also included 16 talks and tutorials by 10 prominent invited speakers, who graciously accepted the Program Committee’s invitation. Title Preface Organization Table of Contents A Grammatical Representation of Visibly Pushdown Languages Introduction Preliminaries Visibly Pushdown Languages Context-Free Grammars Balanced Grammars Grammars for Visibly Pushdown Languages Quasi Balanced Grammars A Grammatical Representation of $\omega$VPLs $\omega$VPL and $\omega$RL(qBL)+$h$ Coincide Conclusion Fully Lexicalized Pregroup Grammars Introduction Background A Preliminary Fact A Pregroup Morphism Properties of Free Pregroup Morphisms Defining a Simulation-Morphism Order-Reflecting Property : Overview and Lemmas Reasoning with Left Derivations Technical Lemmas Main Results Conclusion Bounded Lattice T-Norms as an Interval Category Introduction The Interval Constructor and the Category POSET Lattices Operators on Bounded Lattices T-Norms and Automorphisms on Bounded Lattices T-Norm Morphisms T−NORM as a Cartesian Category Terminal Object Cartesian Product T−NORM as an Interval Category The Functor $\II$ The Natural Transformation $m$ The Functor $F$ The Interval Category FinalRemarks References Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps Introduction The Description Language A New Tool for Analyzing Search Spaces The Algorithm Comparison with Existing Approaches Case Studies Characterizing Sequences Detecting Satisfiability and Building Models Generating Inductive Lemmata Conclusion Continuation Semantics for Symmetric Categorial Grammar Background The Lambek-Grishin Calculus Proofs and Terms LG Sequent Calculus Interpretation: Continuation Semantics Application: Scope Construal Conclusions, Further Directions Shorthand Format for Sequent Derivations Ehrenfeucht–Fra ̈ıss ́e Games on Linear Orders ``Total Information'' Is Sufficient for the EF Game Semimodels and the Complexity of Deciding $Th(LO)$ Hybrid Logical Analyses of the Ambient Calculus Introduction Mobile Ambients Hybrid Logic Modelling Ambients in Hybrid Logic The Naive Analysis The Not-So-Naive Analysis A Better Analysis Complexity Issues and Future Work Structured Anaphora to Quantifier Domains: A Unified Account of Quantificational and Modal Subordination Introduction: Quantificational Subordination Plural Compositional DRT (PCDRT) Plural Information States The Outline of the Proposed Account DRS's and Conditions in PCDRT Compositionality Generalized Quantification in PCDRT Structured Inclusion Maximization and Distributivity Generalized Quantifiers and Indefinites Singular Number Morphology Quantificational Subordination in PCDRT A Parallel Account of Modal Subordination Comparison with Previous Approaches On Principal Types of BCK-λ-Terms Introduction Background The Relevance Relation $\beta_S$-Normal Forms Standardized $(\beta_I\beta_S+{\mathbf K})$-Normal Forms Computing the Principal Types Discards and Discarding Variables The Dependence Relation A Finite-State Functional Grammar Architecture Introduction Discourse Plans Generalized Categorial Dependency Grammars Finite State Converters of F-Trees into D-Structures DP-DS Converters Conclusion Pregroup Calculus as a Logic Functor Introduction Preliminaries Pregroups Free Pregroups Categorial Grammars and Languages Towards a Logic Functor Extending Formulas Discussing a First Axiomatization : $\SAOne$ Defining a Second Axiomatization: $\SA$ for $\myFPG$ Extending Pregroup Calculus to a Logic Functor : Properties Properties of $\SA$ Properties of Composed Calculii Cut Elimination in $\SAc$ : Proof Details Conclusion and Perspectives Appendix: Lemma in $\SA$ and $\SAc$ : Proof Details Lemma1 [$I_R^{-1}$]: Proof by Induction on Derivations of Lemma1 [$IND_L$] We Prove That: Lemma2 : We Prove, Using Lemma1 That Lemma1 [$IND_R-$] Proof by Induction, According to $R_l$ of: Proof of Lemma4: $[IND_R]$ and $[A_R]$ (also $[A_{R+}]$) Are Admissible Rules in $\SAc$ A Formal Calculus for Informal Equality with Binding Introduction Syntax A Derivation System Semantics Soundness and Completeness Related Work Conclusions Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm Introduction Geometric Framework KB2D Formal Verification of KB2D Geometrical Analysis Correctness of Resolution Optimality Correctness of Recovery Coordinated Maneuvers Conclusions and Future Work An Introduction to Context Logic Introduction What Is Context Logic? Extending Context Logic Structured Data Models Sequences Heaps and Stores Trees Terms Additional Work Numerical Constraints for XML Introduction Numerical XML Constraints The XML Tree Model Path Languages Numerical Constraints Satisfiability and Implication Computational Intractability Numerical Keys Numerical Key Implication Axiomatisation Time-Complexity of Deciding Implication Updating, Encrypting and Indexing Conclusion and Future Work Modules over Monads and Linearity Introduction Monads and Algebras Modules over Monads Left Modules Right Modules Limits and Colimits of Left Modules Base Change Initial Algebra Semantics Monads over Sets Untyped Syntactic Lambda Calculus Untyped Semantic Lambda Calculus Monads over Types Typed Lists Simply Typed Lambda Calculus Typed Lambda Calculus Monads over Preordered Sets Conclusions and Related Works Appendix: Formal Proof of Theorem 3 Structure of the Formalisation Formalisation of Monads and Modules Formalisation of the $\lambda$ -Calculus Proof of the Main Theorem Hydra Games and Tree Ordinals Introduction Tree Ordinals Hydra Games The Correspondence Conclusion Spin Networks, Quantum Topology and Quantum Computation Introduction Spin Networks and Temperley -- Lieb Recoupling Theory Evaluations Symmetry and Unitarity Quantum Computation of Colored Jones Polynomials and the Witten-Reshetikhin-Turaev Invariant Symmetries in Natural Language Syntax and Semantics: The Lambek-Grishin Calculus Background Lambek-Grishin Calculus Decidable Proof Search The Group of Grishin Interactions Type Similarity Relational Semantics Computational Semantics Linguistic Applications Conclusions Admissibility of Cut Computational Interpretations of Classical Linear Logic Introduction Classical Linear Logic $\LLomega$ Basic Interpretation Completeness Possible Interpretations of Exponentials Interpretation 1: Kreisel's Modified Realizability Interpretation 2: Diller-Nahm Interpretation Interpretation 3: Stein's Interpretation Interpretation 4: Bounded Dialectica Interpretation Interpretation 5: Gödel's Dialectica Interpretation Autonomous Programmable Biomolecular Devices Using Self-assembled DNA Nanostructures Introduction Why Computer Science Is Relevant to the Nano-scale Introducing DNA Nanotechnology and Its Use to Assemble Molecular-Scale Devices Adelman’s Initial Demonstration of a DNA-Based Computation Adleman’s Experiment The Non-scalability of Adelman ‘s Experiment Autonomous Biomolecular Computation Self-assembled DNA Tiles and Lattices Computation by Self-assembly DNA Tiles and Lattices Autonomous Finite State Computation Using Linear DNA Nanostructures The First Experimental Demonstration of Autonomous Computations Using Self-assembly of DNA Nanostructures Autonomous Finite-State Computations Via Disassembly of DNA Nanostructures Conclusions References Interval Valued QL-Implications Introduction Interval Representations Best Interval Representation Interval t-norm and Interval t-conorm Interval Fuzzy Negation Fuzzy Implication QL-Implication Interval Fuzzy Implication Interval QL-Implication Propagation of an Interval Uncertainty in Interval QL-Implications Interval Automorphism Canonical Construction of an Interval Automorphism The Best Interval Representation of an Automorphism Interval Automorphism Acting on Interval QL-Implication Conclusion and Final Remarks Behavioural Differential Equations and Coinduction for Binary Trees Introduction Trees and Coinduction Behavioural Differential Equations Tree Calculus Applications of Tree Calculus Discussion Proof of Theorem 2 A Sketch of a Dynamic Epistemic Semiring Introduction Modal Semirings Dynamic Epistemic Semirings A Relational Model for Revision A Basic Calculus Deriving the AGM Axioms for Revision Concluding Remarks Detailed Proofs A Modal Distributive Law (abstract) Ant Colony Optimization with Adaptive Fitness Function for Satisfiability Testing Introduction The SAT Problem Ant Colony Optimization Construction of Assignments by Ants Updating Pheromone Values Adaptive Fitness Functions Stepwise Adaptation of Weights (SAW) Refining Functions (RF) Experimental Results Environment Comparative Results Conclusions and Future Work Author Index Welcome to the proceedings of the 14th WoLLIC meeting, which was held in Rio de Janeiro, Brazil, July 2 - 5, 2007. The Workshop on Logic, Language, Information and Computation (WoLLIC) is an annual international forum on inter-disciplinary research involving formal logic, computing and programming theory, and natural language and reasoning. The WoLLIC meetings alternate between Brazil (and Latin America) and other countries, with the aim of fostering interest in applied logic among Latin Am- ican scientists and students, and facilitating their interaction with the international - plied logic community. WoLLIC 2007 focused on foundationsof computing and programming, novel c- putation models and paradigms, broad notions of proof and belief, formal methods in software and hardware development; logical approaches to natural language and r- soning; logics of programs, actions and resources; foundational aspects of information organization, search,?ow, sharing, and protection. The Program Committee for this meeting, consisting of the 28 colleagues listed here, was designed to promote these inter-disciplinary and cross-disciplinary topics. Like its predecessors, WoLLIC 2007 included invited talks and tutorials as well as contributed papers. The Program Committee received 52 complete submissions (aside from 15 preliminary abstracts which did not materialize). A thorough review process by the Program Committee, assisted by over 70 external reviewers, led to the acc- tance of 21 papers for presentation at the meeting and inclusion in these proceedings. The conference program also included 16 talks and tutorials by 10 prominent invited speakers, who graciously accepted the Program Committee's invitation This book constitutes the refereed proceedings of the 14th International Workshop on Logic, Language, Information and Computation, WoLLIC 2007, held in Rio de Janeiro, Brazil in July 2007. The 21 revised full papers presented together with 5 invited papers were carefully reviewed and selected from 52 submissions. The papers focus on foundations of computing and programming, novel computation models and paradigms, broad notions of proof and belief, formal methods in software and hardware development; logical approach to natural language and reasoning; logics of programs, actions and resources; foundational aspects of information organization, search, flow, sharing, and protection