COLOG-88

1. Front Matter

   PDF

2. Algebraic specified processes and enumerable models

   • Morozov Andrey

   Pages 1-2

3. On conditions of full coherence in biclosed categories: A new application of proof theory

   • A. A. Babaev, S. V. Soloviev

   Pages 3-8

4. The use of justification systems for integrated semantics

   • N. G. de Brujin

   Pages 9-24

5. An equational deductive system for the differential and integral calculus

   • Rolando Chuaqui, Patrick Suppes

   Pages 25-49

6. Inductively defined types

   • Thierry Coquand, Christine Paulin

   Pages 50-66

7. Algorithms for probabilistic inference

   • E. Ya. Dantsin

   Pages 67-75

8. Geometry of interaction 2: Deadlock-free algorithms

   • Jean-Yves Girard

   Pages 76-93

9. On the syntax of infinite objects: an extension of Martin-Löf's theory of expressions

   • Lars Hallnäs

   Pages 94-104

10. β-Reductions and β-developments of λ-terms with the least number of steps

    • Zurab O. Khasidashvili

    Pages 105-111

11. Group-theoretic approach to intractable problems

    • V. Ya. Kreinovich

    Pages 112-121

12. On some applications of Heyting-valued analysis II

    • V. A. Lyubetsky

    Pages 122-145

13. Mathematics of infinity

    • Per Martin-Löf

    Pages 146-197

14. Gentzen-type systems and resolution rules part I propositional logic

    • G. Mints

    Pages 198-231

15. On the problem of reducing search in logic program execution

    • V. S. Neiman

    Pages 232-241

16. Correctness of short proofs in theory with notions of feasibility

    • V. P. Orevkov

    Pages 242-245

17. A formulation of the simple theory of types (for Isabelle)

    • Lawrence C. Paulson

    Pages 246-274

18. On connections between classical and constructive semantics

    • Starchenko S. S., Voronkov A. A.

    Pages 275-285

19. Flow-diagrams with sets

    • Alexey P. Stolboushkin

    Pages 286-299

20. The resolution program, able to decide some solvable classes

    • Tanel Tammet

    Pages 300-312

This volume contains several invited papers as well as a selection of the other contributions. The conference was the first meeting of the Soviet logicians interested in com- puter science with their Western counterparts. The papers report new results and techniques in applications of deductive systems, deductive program synthesis and analysis, computer experiments in logic related fields, theorem proving and logic programming. It provides access to intensive work on computer logic both in the USSR and in Western countries.

• Beweissysteme
• UdSSR
• logic
• programming
• proving
• theorem proving

Policies and ethics