Computer Science Logic: 5th Workshop, CSL ’91 Berne, Switzerland, October 7–11, 1991 Proceedings

Yaniv Bargury, Johann Makowsky (auth.), Egon Börger, Gerhard Jäger, Hans Kleine Büning, Michael M. Richter (eds.)354055789X, 9783540557890

This volume presents the proceedings of the workshop CSL ’91 (Computer Science Logic) held at the University of Berne, Switzerland, October 7-11, 1991. This was the fifth in a series of annual workshops on computer sciencelogic (the first four are recorded in LNCS volumes 329, 385, 440, and 533). The volume contains 33 invited and selected papers on a variety of logical topics in computer science, including abstract datatypes, bounded theories, complexity results, cut elimination, denotational semantics, infinitary queries, Kleene algebra with recursion, minimal proofs, normal forms in infinite-valued logic, ordinal processes, persistent Petri nets, plausibility logic, program synthesis systems, quantifier hierarchies, semantics of modularization, stable logic, term rewriting systems, termination of logic programs, transitive closure logic, variants of resolution, and many others.

---

Table of contents :
The expressive power of transitive closure and 2-way multihead automata….Pages 1-14
Correctness proof for the WAM with types….Pages 15-34
Model checking of persistent Petri nets….Pages 35-52
Provability in TBLL: A decision procedure….Pages 53-67
How to implement first order formulas in local memory machine models….Pages 68-78
A new approach to abstract data types II computation on ADTs as ordinary computation….Pages 79-95
A primitive recursive set theory and AFA: On the logical complexity of the largest bisimulation….Pages 96-110
On bounded theories….Pages 111-118
The cutting plane proof system with bounded degree of falsity….Pages 119-133
Denotational versus declarative semantics for functional programming….Pages 134-148
On transitive closure logic….Pages 149-163
Some aspects of the probabilistic behavior of variants of resolution….Pages 164-172
Safe queries in relational databases with functions….Pages 173-183
Logical inference and polyhedral projection….Pages 184-200
Stable logic….Pages 201-212
A transformational methodology for proving termination of logic programs….Pages 213-226
Plausibility logic….Pages 227-241
Towards Kleene Algebra with recursion….Pages 242-256
Equational specification of abstract types and combinators….Pages 257-271
Normal forms in infinite-valued logic: The case of one variable….Pages 272-277
A fragment of first order logic adequate for observation equivalence….Pages 278-292
Ordinal processes in comparative concurrency semantics….Pages 293-305
Logical semantics of modularisation….Pages 306-315
A cut-elimination procedure designed for evaluating proofs as programs….Pages 316-325
Minimal from classical proofs….Pages 326-328
Quantifier hierarchies over word relations….Pages 329-338
Complexity results for the default- and the autoepistemic logic….Pages 339-352
On Completeness for NP via projection translations….Pages 353-366
Control of ω-automata, Church’s problem, and the emptiness problem for tree ω-automata….Pages 367-381
Comparing the theory of representations and constructive mathematics….Pages 382-395
Infinitary queries and their asymptotic probabilities I: Properties definable in transitive closure logic….Pages 396-410
On completeness of program synthesis systems….Pages 411-418
Proving termination for term rewriting systems….Pages 419-428