Logical Foundations of Computer Science - Tver '92: Second International Symposium, Tver, Russia, July 20-24, 1992. Proceedings (Lecture Notes in Computer Science)

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.--publisher's Website. Modal Linear Logic / D.a. Archangelsky, M.a. Taitslin -- Machine Learning Of Higher Order Programs / G. Baliga [and Others] -- Quantifying The Amount Of Verboseness / R. Beigel, M. Kummer, F. Stephan -- Strictness Logic And Polymorphic Invariance / P.n. Benton -- Preference Logics And Non-monotonicity In Logic Programming / A.l. Brown, Jr., S. Mantha, T. Wakayama -- The Ehrenfeucht-fraisse Games For Transitive Closure / A. Calo, J.a. Makowsky -- Feasibility Of Finite And Infinite Paths In Data Dependent Programs / K. Cerans -- An Interleaving Model For Real-time Systems / L. Chen -- A Logical Characterization Of Asynchronously Communicating Agents / S. Christensen -- Denotations For Classical Proofs -- Preliminary Results / P. De Groote -- Ordinal Arithmetic With List Structures / N. Dershowitz, E.m. Reingold -- Continuous I-categories / A. Edalat -- Many-valued Non-monotonic Modal Logics / M. Fitting --^ Automated Deduction In Additive And Multiplicative Linear Logic / D. Galmiche, G. Perrier -- Intensionally ̃stable Functions / B. Gamatie -- A Constructive Proof That Trees Are Well-quasi-ordered Under Minors / A. Gupta -- Banishing Robust Turing Completeness / L.a. Hemachandra, S. Jain, N.k. Vereshchagin -- Balanced Formulas, Bck-minimal Formulas And Their Proofs / S. Hirokawa -- Non-stable Models Of Linear Logic / R. Hoofman -- Ordering Optimizations For Concurrent Logic Programs / A. King, P. Soper -- A Categorical Interpretation Of Partial Function Logic And Hoare Logic / P.m.w. Knijnenburg, F. Nordemann -- The Polynomial Complexity Of Conjunctive Normal Form Satisfiability, When The Number Of Conjunctions And Negations Is Limited / N.k. Kossovsky, A.b. Prokhoroff -- Typed [lambda]-calculus With Recursive Definitions / S.v. Kotov -- Set Theoretic Foundations For Fuzzy Set Theory, And Their Applications / K. Lano --^ Constructive Specifications Of Abstract Data Types Using Temporal Logic / F. Lesske -- An Interval-based Modal Logic For System Specification / R. Li, J. Carmo -- A Unifying Theory Of Dependent Types / Z. Luo -- Msl -- A Mathematical Specification Language / V.p. Makarov -- Partial Algebra + Order-sorted Algebra = Galactic Algebra / A. Megrelis -- Minimal Negation And Hereditary Harrop Formulae / A. Momigliano -- Kleene Automata And Recursion Theory / J. Mullins -- Incremental Polymorphic Type Checking With Update / A. Mycroft -- Operators On Lattices Of [omega]-herbrand Interpretations / J.a. Plaza -- Sequential Calculus For Proving The Properties Of Regular Programs / A. Pliuskeviciene -- Complete Sequential Calculi For The First Order Symmetrical Linear Temporal Logic With Until And Since / R. Pliuskevicius -- Non Modularity And Expressibility For Nets Of Relations / A. Rabinovich -- Correctness Of Generic Modules / W. Reif --^ An And-parallelism Cooperative Scheme For Full Prolog Interpreters On A Transputer-based Architecture / K. Sadi, F. Meunier -- A Sequent Calculus For A First Order Linear Temporal Logic With Equality / J. Sakalauskaite -- On The Expressive Power Of Modal Logics On Trees / B.-h. Schlingloff -- Propositional Dynamic Logic With Fixed Points / N.v. Shilov -- Effective Operators And Continuity Revisited / D. Spreen -- Logical Characterizations Of Bounded Query Classes I / I.a. Stewart -- Solving Equational Constraints In Polymorphic Types / J. Tiuryn -- Gentzen-style And Novikov-style Cut-elimination / S. Tupailo -- Graded Modalities In Epistemic Logic / W. Van Der Hoek, J.-j. Ch. Meyer. A. Nerode, M. Taitslin (eds.). Includes Bibliographical References. 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