Logic, Language, Information and Computation: 17th International Workshop, WoLLIC 2010, Brasilia, Brazil, July 6-9, 2010, Proceedings (Lecture Notes in Artificial Intelligence, Vol. 6188)

✍ Scribed by Anuj Dawar (editor), Ruy de Queiroz (editor)

• Publisher: Springer
• Year: 2010
• Tongue: English
• Leaves: 268
• Category: Library

✦ Synopsis

This volume contains the papers presented at WoLLIC 2010: 17th Workshop on Logic, Language, Information and Computation held during July 6–9, 2010, on the campus of Universidade de Bras´ ?lia (UnB), Brazil. The Workshop on Logic, Language, Information and Computation (WoL- LIC) is an annual event, meeting every year since 1994, which aims at fostering interdisciplinary research in pure and applied logic. The idea is to have a forum which is large enough in the number of possible interactions between logic and the sciences related to information and computation, and yet is small enough to allow for concrete and useful interaction among participants. The present volume contains 13 contributed papers that were selected from among 32 submissions after a rigorous review by the Program Committee. Each submission was reviewed by at least two, and on average three, Program C- mittee members. This volume also containspapersor abstractsthat relateto the seven invited talks presented at the workshop. Between them, these papers give a snapshot of some fascinating work taking place at the frontiers between computation, logic, and linguistics. We are grateful to all the people who made this meeting possible and are responsible for its success: the members of the Program Committee and the external reviewers, the invited speakers, the contributors, and the people who were involved in organizing the workshop.

✦ Table of Contents

Title
Preface
Organization
Table of Contents
Entailment Multipliers: An Algebraic Characterization of Validity for Classical and Modal Logics
Introduction
Comparisons with the Literature
Organisation of the Paper
Entailment Multipliers
Multipliers and the NP = coNP Problem
Strengthening Entailment Expressions
Computing Entailment Multipliers
Resolution
Sequent Calculus
Multipliers for Normal Modal Logics
Conclusion
References
A CTL-Based Logic for Program Abstractions
Introduction
CTL with Path Relativisation
Examples
Results on CTLrel
Expressivity
Model Checking
Satisfiability
CTL with Path Relativisation in Abstraction
A Suffix Heuristic
A Local Heuristic
Conclusion and Further Work
References
Application of Logic to Integer Sequences:A Survey
Sequences of Integers and Their Combinatorial Interpretations
Linear Recurrences
Logical Interpretations and Linear Recurrences
P-Recursive (Holonomic) Sequences
References
The Two-Variable Fragment with Counting Revisited
Introduction
Preliminaries
A Result on Solutions to Integer Programming Problems
The Main Result
References
Intuitionistic Logic and Computability Theory
Tutorial 1: Intuitionistic Logic
Tutorial 2: Computability Theory
Computability Theoretic Interpretations of Intuitionistic Logic
References
Foundations of Satisfiability Modulo Theories
Logical Form as a Determinant of Cognitive Processes
Introduction
Why Logic Has Come to Be Seen as Irrelevant for Cognitive Science
Marr's Levels of Explanation and Logic
A Common Failure in Psychiatric Disorders: Executive Function
Logic and Executive Function
Non-monotonicity in Autism: Rules and Exceptions
Theory of Mind and Reasoning
Reasoning in the False Belief Task
Executive Dysfunction and the Box Task
The Suppression Task as a Formal Analogue of the Box Task
A Formal Analysis
Autists and the Suppression Task
An Apparent Counterexample: The Tubes Task' Conclusion: The Role of Logic in Cognitive Processes References Formal Lifetime Reliability Analysis Using Continuous Random Variables Introduction Related Work Statistical Properties of Lifetime Distributions Verification of Statistical Properties Moments and Variance of Lifetime Distributions Reliability Theory Formalization Survival Function Hazard Function Reliability Analysis of a Capacitor Capacitor Lifetime Model Verification of Reliability Properties Conclusions References Modal Logics with Counting Counting, Modally Representing Plurals in Natural Language The Expressive Power of MLC Inference in MLC Conclusions References Verification of the Completeness of Unification Algorithmsa la Robinson
Introduction
Basic Notions on First-Order Unification
Specification of Basic Notions
Specification of Unification Algorithms
Reusing the Proof Technology: Termination and Soundness
Treatment of Exceptions: Proof of Completeness
Related Work
Conclusions and Future Work
References
Mechanisation of PDA and Grammar Equivalence for Context-Free Languages
Introduction
Context-Free Grammars
Pushdown Automata
Constructing a PDA for a CFG
Constructing a CFG from a PDA
Proof of the if'' portion of (2) Proof of theonly if'' portion of (2)
Related Work and Conclusions
References
On the Role of the Complementation Rule for Data Dependencies over Incomplete Relations
Introduction
Related Work
Preliminaries
Appropriate Reasoning
Undetermined Universes
Conclusion
References
Decidability and Undecidability Resultson the Modal μ-Calculus with a Natural Number-Valued Semantics
Introduction
Preliminaries
Syntax and Semantics
Application of the Semantics
Undecidability
Decidability
Outline of the Decidability Proof
Translation
Conclusions
References
Appendix: Translation Examples
Solving the Implication Problem for XML Functional Dependencies with Properties
Introduction
Related Work
Preliminaries
XML Functional Dependencies with Properties
The Semantic Equivalence Theorem
An Example for Applying the Semantic Equivalence
Conclusion and Future Directions
References
Appendix
On Anaphora and the Binding Principles in Categorial Grammar
Introduction
Displacement Calculus
Reflexives and Principle A
Personal Pronouns and Principle B
Principle C
Conclusion
References
Feasible Functions over Co-inductive Data
Introduction
Background
Equational and Relational Programs
A Logical Characterization of Correct Computability
Formal Reasoning about Inductive and Coinductive Data
Coinduction
Functional Representation in L*+
Examples
The Basic Feasible Functionals Are Provable in Ramified Second Order Logic
Basic Feasible Functionals
BFF Is Provable in Ramified Second Order Logic
References
Interval Valued Fuzzy Coimplication
Introduction
Preliminary Studies
Best Interval Representation
Interval Fuzzy Negations
Interval Fuzzy t-Norms and t-Conorms
Interval Fuzzy Coimplications
Properties of Interval Coimplications and Duality Relationships
Duality Relationships Preserved by Canonical Representation
Border and Model Interval Fuzzy Coimplications
Conclusion and Final Remarks
References
Reduction of the Intruder Deduction Problem into Equational Elementary Deduction for Electronic Purse Protocols with Blind Signatures
Introduction
Modeling Intruder Deduction for the Electronic Purse Protocol with Blind Signatures
Syntax
The Electronic Purse Protocol: The Equational Theory EP
The Convergent Rewriting System R Equivalent to the Equational Theory EP
Sequent Calculus for the Intruder
Elementary Intruder Deduction under the EP Theory
Conclusion
References
Intersection Type Systems and Explicit Substitutions Calculi
Introduction
-Calculus with de Bruijn Indices
The se-Calculus
The -Calculus
Intersection Type Systems for the dB-Calculus
The System dBSM
Subject Reduction for System dBSM
An Intersection Type System for se
The System sSM
The System se
An Intersection Type System for
Conclusion
References
Generalising Conservativity
Introduction
Some Arity Reducers
Conservativity
Other Constraints
Conclusion
References
Author Index