Logical Foundations of Computer Science: International Symposium, LFCS 2007, New York, NY, USA, June 4-7, 2007. Proceedings

Evangelia Antonakos (auth.), Sergei N. Artemov, Anil Nerode (eds.)3540727329, 9783540727323, 9783540727347

This book constitutes the refereed proceedings of the International Symposium on Logical Foundations of Computer Science, LFCS 2007, held in New York, NY, USA in June 2007.

The volume presents 36 revised refereed papers carefully selected by the program committee. It addresses all current aspects of logic in computer science, including constructive mathematics and type theory, logical foundations of programming, logical aspects of computational complexity, logic programming and constraints, automated deduction and interactive theorem proving, logical methods in protocol and program verification and in program specification and extraction, domain theory logics, logical foundations of database theory, equational logic and term rewriting, lambda and combinatory calculi, categorical logic and topological semantics, linear logic, epistemic and temporal logics, intelligent and multiple agent system logics, logics of proof and justification, nonmonotonic reasoning, logic in game theory and social software, logic of hybrid systems, distributed system logics, system design logics, as well as other logics in computer science.

---

Table of contents :
Front Matter….Pages –
Justified and Common Knowledge: Limited Conservativity….Pages 1-11
The Intensional Lambda Calculus….Pages 12-25
Generalized Non-deterministic Matrices and (n,k)-ary Quantifiers….Pages 26-40
Elementary Differential Calculus on Discrete and Hybrid Structures….Pages 41-53
Weighted Distributed Systems and Their Logics….Pages 54-68
Weighted O-Minimal Hybrid Systems Are More Decidable Than Weighted Timed Automata!….Pages 69-83
On Decidability and Expressiveness of Propositional Interval Neighborhood Logics….Pages 84-99
Reasoning About Sequences of Memory States….Pages 100-114
Cut Elimination in Deduction Modulo by Abstract Completion….Pages 115-131
Density Elimination and Rational Completeness for First-Order Logics….Pages 132-146
Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus….Pages 147-161
Topological Semantics and Bisimulations for Intuitionistic Modal Logics and Their Classical Companion Logics….Pages 162-179
A Decidable Temporal Logic of Repeating Values….Pages 180-194
Model Checking Knowledge and Linear Time: PSPACE Cases….Pages 195-211
Realizations and LP ….Pages 212-223
Successive Abstractions of Hybrid Automata for Monotonic CTL Model Checking….Pages 224-240
Explicit Proofs in Formal Provability Logic….Pages 241-253
A Synthesis Algorithm for Hybrid Systems….Pages 254-268
Including the Past in ‘Topologic’….Pages 269-283
A Note on Rewriting Proofs and Fibonacci Numbers….Pages 284-292
On Complexity of Ehrenfeucht-Fraïssé Games….Pages 293-309
The Law of the Iterated Logarithm for Algorithmically Random Brownian Motion….Pages 310-317
Hypersequent Calculus for Intuitionistic Logic with Classical Atoms….Pages 318-331
Proof Identity for Classical Logic: Generalizing to Normality….Pages 332-348
On the Constructive Dedekind Reals: Extended Abstract….Pages 349-362
Verifying Balanced Trees….Pages 363-378
Compactness Properties for Stable Semantics of Logic Programs….Pages 379-400
Uniform Circuits, & Boolean Proof Nets….Pages 401-421
Finite Automata Presentable Abelian Groups….Pages 422-436
Embeddings into Free Heyting Algebras and Translations into Intuitionistic Propositional Logic….Pages 437-448
Some Puzzles About Probability and Probabilistic Conditionals….Pages 449-456
A Temporal Dynamic Logic for Verifying Hybrid System Invariants….Pages 457-471
Multiplexor Categories and Models of Soft Linear Logic….Pages 472-485
Until-Since Temporal Logic Based on Parallel Time with Common Past. Deciding Algorithms….Pages 486-497
Total Public Announcements….Pages 498-511
Back Matter….Pages –