Logical Foundations of Computer Science — Tver ’92: Second International Symposium Tver, Russia, July 20–24, 1992 Proceedings

Dimitry A. Archangelsky, Mikhail A. Taitslin (auth.), Anil Nerode, Mikhail Taitslin (eds.)3540557075, 9783540557074

This volume presents the papers selected for the Symposium Logic at Tver ’92, held at Sokol, near Tver, Russia in July 1992. It is the second in a series of international symposia on logical foundations of computer science held in Russia. The meeting is a joint effort of scholars from both the former Soviet Union and the West, and indicates a new era of international cooperation. Sponsors of the meeting include: the Association for Computing Machinery, the Association for Symbolic Logic, andthe Committee on Mathematical Foundations of Computer Science of IEEE. The book is a unique source of information on the state of computer science research in the former Soviet Union and presents important discoveries in the area of logical foundations of computer science.

---

Table of contents :
Modal Linear Logic….Pages 1-8
Machine learning of higher order programs….Pages 9-20
Quantifying the amount of verboseness (extended abstract)….Pages 21-32
Strictness logic and polymorphic invariance….Pages 33-44
Preference logics and nonmonotonicity in logic programming….Pages 45-56
The Ehrenfeucht-Fraïssé games for transitive closure….Pages 57-68
Feasibility of finite and infinite paths in data dependent programs….Pages 69-80
An interleaving model for real-time systems….Pages 81-86
Incremental evaluation of natural semantics specifications….Pages 87-104
Denotations for classical proofs -Preliminary results-….Pages 105-116
Ordinal arithmetic with list structures (preliminary version)….Pages 117-138
Many-valued non-monotonic modal logics….Pages 139-150
Automated deduction in additive and multiplicative linear logic….Pages 151-162
Intensionally stable functions….Pages 163-173
A constructive proof that tree are well-quasi-ordered under minors (detailed abstract)….Pages 174-185
Banishing robust Turing completeness….Pages 186-197
Balanced formulas, BCK-minimal formulas and their proofs….Pages 198-208
Non-stable models of linear logic….Pages 209-220
Ordering optimisations for concurrent logic programs….Pages 221-228
A categorical interpretation of partial function logic and Hoare logic….Pages 229-240
The polynomial complexity of conjunctive normal form satisfiability, when the number of conjunctions and negations is limited….Pages 241-245
Typed λ-calculus with recursive definitions….Pages 246-257
Set theoretic foundations for fuzzy set theory, and their applications….Pages 258-268
Constructive specifications of abstract data types using temporal logic….Pages 269-280
An interval-based modal logic for system specification….Pages 281-292
A unifying theory of dependent types: the schematic approach….Pages 293-304
MSL — A Mathematical Specification Language….Pages 305-313
Partial algebra + order-sorted algebra = galactic algebra….Pages 314-325
Minimal negation and Hereditary Harrop formulae….Pages 326-335
Kleene automata and recursion theory….Pages 336-346
Incremental polymorphic type checking with update….Pages 347-357
Operators on lattices of ω-Herbrand interpretations….Pages 358-369
Sequential calculus for proving the properties of regular programs….Pages 370-381
Complete sequential calculi for the first order symmetrical linear temporal logic with until and since….Pages 382-393
Non modularity and expressibility for nets of relations (extended abstract)….Pages 394-405
Correctness of generic modules….Pages 406-417
An and-parallelism cooperative scheme for full prolog interpreters on a transputer-based architecture….Pages 418-429
A sequent calculus for a first order linear temporal logic with equality….Pages 430-440
On the expressive power of modal logics on trees….Pages 441-451
Propositional dynamic logic with fixed points: Algorithmic tools for verification of finite state machines….Pages 452-458
Effective operators and continuity revisited….Pages 459-469
Logical characterizations of bounded query classes I: Logspace oracle machines….Pages 470-479
Solving equational constraints in polymorphic types….Pages 480-492
Gentzen-style and Novikov-style cut-elimination….Pages 493-502
Graded modalities in epistemic logic….Pages 503-514