Logical Foundations of Computer Science: 4th International Symposium, LFCS’97 Yaroslavl, Russia, July 6–12, 1997 Proceedings

Sergei Artemov, Jennifer Davoren, Anil Nerode (auth.), Sergei Adian, Anil Nerode (eds.)3540630457, 9783540630456

This book constitutes the refereed proceedings of the 4th International Symposium on Logical Foundations of Computer Science, LFCS’97, held in Yaroslavl, Russia, in July 1997.
The volume presents 42 revised refereed papers carefully selected by the program committee. All current issues of computer science logic are addressed. There is a certain emphasis on reporting the progress achieved by scientists from various parts of the former Soviet Union; but there are also many other strong papers from the international research community.

---

Table of contents :
Topological semantics for hybrid systems….Pages 1-8
Domain-free pure type systems….Pages 9-20
Generic queries over quasi- o -minimal domains….Pages 21-32
Towards computing distances between programs via Scott domains….Pages 33-43
A safe recursion scheme for exponential time….Pages 44-52
Finite model theory, universal algebra and graph grammars….Pages 53-55
Complexity of query answering in logic databases with complex values….Pages 56-66
Recognition of deductive data base stability….Pages 67-77
The concurrency complexity for the Horn fragment of linear logic….Pages 78-87
Studying algorithmic problems for free semi-groups and groups….Pages 88-101
Learning small programs with additional information….Pages 102-112
Cut elimination for the second order propositional logic with Hilbert’s ε-symbol, extensionality, and full comprehension….Pages 113-118
Finite bases of admissible rules for the logic S 5 2 C ….Pages 119-129
An algebraic correctness criterion for intuitionistic proof-nets….Pages 130-140
Towards a theory of recursive structures….Pages 141-144
On the complexity of prefix formulas in modal logic of subset spaces….Pages 145-155
The undecidability of second order linear affine logic….Pages 156-166
Operational logic of proofs with functionality condition on proof predicate….Pages 167-177
On linear ordering of strongly extensional finitely-branching graphs and non-well-founded sets….Pages 178-188
Functions for the general solution of parametric word equations….Pages 189-202
A proof procedure for hereditary Harrop formulas with free equality….Pages 203-213
Basic forward chaining construction for logic programs….Pages 214-225
Decidability and undecidability of the halting problem on Turing machines, a survey….Pages 226-236
Case study: Additive linear logic and lattices….Pages 237-247
Some decision problems for traces….Pages 248-257
Existential instantiation and strong normalization….Pages 258-265
Models for the logic of proofs….Pages 266-275
Interpretation of the full computation tree logic CTL * on sets of infinite sequences….Pages 276-282
Type introduction for equational rewriting….Pages 283-293
Capturing bisimulation-invariant Ptime….Pages 294-305
Equivalence of multiplicative fragments of cyclic linear logic and noncommutative linear logic….Pages 306-311
A decidable fragment of second order linear logic….Pages 312-322
Some results on Propositional Dynamic Logic with fixed points….Pages 323-332
Quasi-characteristic inference rules for modal logics….Pages 333-341
Provability logic with operations on proofs….Pages 342-353
Formal verification of logic programs: Foundations and implementation….Pages 354-368
Unification of terms with term-indexed variables….Pages 369-373
Back-forth equivalences for design of concurrent systems….Pages 374-384
Association nets: An alternative formalization of common thinking….Pages 385-398
Simulating η-expansions with Β-reductions in the second-order polymorphic λ-rcalculus….Pages 399-409
Logical schemes for first order theories….Pages 410-418
Verification of PLTL formulae by means of monotone disjunctive normal forms….Pages 419-429