Logic for Concurrency and Synchronisation

The study of information-based actions and processes has been a vibrant - terface between logic and computer science for several decades now. Indeed, several natural perspectives come together here. On the one hand, logical s- tems may be used to describe

  • PDF / 14,173,404 Bytes
  • 298 Pages / 432 x 684 pts Page_size
  • 7 Downloads / 193 Views

DOWNLOAD

REPORT


TRENDS IN LOGIC

Studia Logica Library VOLUME 18 Managing Editor Ryszard Wójcicki, Institute of Philosophy and Sociology, Polish Academy of Sciences, Warsaw, Poland Editors Daniele Mundici, Department of Mathematics “Ulisse Dini”, University of Florence, Italy Ewa Orlowska, National Institute of Telecommunications, Warsaw, Poland Graham Priest, Department of Philosophy, University of Queensland, Brisbane, Australia Krister Segerberg, Department of Philosophy, Uppsala University, Sweden Alasdair Urquhart, Department of Philosophy, University of Toronto, Canada Heinrich Wansing, Institute of Philosophy, Dresden University of Technology, Germany

SCOPE OF THE SERIES Trends in Logic is a bookseries covering essentially the same area as the journal Studia Logica – that is, contemporary formal logic and its applications and relations to other disciplines. These include artificial intelligence, informatics, cognitive science, philosophy of science, and the philosophy of language. However, this list is not exhaustive, moreover, the range of applications, comparisons and sources of inspiration is open and evolves over time.

Volume Editor Heinrich Wansing

The titles published in this series are listed at the end of this volume.

LOGIC FOR CONCURRENCY AND SYNCHRONISATION Edited by

RUY J.G.B. DE QUEIROZ Universidade Federal de Pernambuco, Recife, Brazil

KLUWER ACADEMIC PUBLISHERS NEW YORK, BOSTON, DORDRECHT, LONDON, MOSCOW

eBook ISBN: Print ISBN:

0-306-48088-3 1-4020-1270-5

©2003 Kluwer Academic Publishers New York, Boston, Dordrecht, London, Moscow Print ©2003 Kluwer Academic Publishers Dordrecht All rights reserved No part of this eBook may be reproduced or transmitted in any form or by any means, electronic, mechanical, recording, or otherwise, without written consent from the Publisher Created in the United States of America Visit Kluwer Online at: and Kluwer's eBookstore at:

http://kluweronline.com http://ebooks.kluweronline.com

Contents

List of Figures

xi

List of Tables

xv

Foreword Johan van Benthem

xvii

Preface

xix

Contributing Authors

xxi

Part I

From a Structural Perspective

1 Geometry of Deduction via Graphs of Proofs Anjolina Grisi de Oliveira and Ruy J. G. B. de Queiroz 1 Motivation Relevance to proof theory: towards the geometry of 1.1 natural deduction 1.2 Relevance to theoretical computer science: complexity and concurrency 2 The idea of studying proofs as geometric objects Representing proofs in a graph 2.1 Some results 2.2 2.2.1 Elementary results on isomorphisms 2.2.2 On the genus of a derivation 2.2.3 On the relationship between the notions of direct proof, normal proof and proof, and the subformula property Proof-nets 3 Criticisms of natural deduction 3.1 3.1.1 Classical symmetry 3.1.2 Global rules 3.1.3 The commutative conversions 3.2 Analyzing the sequent calculus 3.2.1 The non-determinism of Hauptsatz 3.2.2 Redundancies in proofs 3.2.3 Non-unicity of proofs Definition of links 3.3

v

3 4

6 8 12 12 16 16 16

17 17 18 18 18 19 19 19 20 20 21

vi

LOGIC FOR CONCURRENCY AND SYNCHR