The study of information-based actions and processes has been a vibrant interface between logic and computer science for decades now. The individual chapters of this book show the state of the art in current investigations of process calculi with mainly two major paradigms at work: linear logic and modal logic. Viewed together, the chapters also offer exciting glimpses of future integration with obvious links including modal logics for proof graphs, labelled deduction merging modal and linear logic, Chu spaces linking proof theory and model theory and bisimulation-style equivalences for analysing proof processes. The combination of approaches and pointers for further integration also suggests a grander vision for the field. In classical computation theory, Church's Thesis provided a unifying and driving force. Likewise, modern process theory would benefit immensely from a synthesis bringing together paradigms like modal logic, process algebra, and linear logic. If this Grand Synthesis is ever going to happen, books like this are needed!
This book is for researchers in computer science, mathematical logic, and philosophical logic. It shows the state of the art in current investigations of process calculi with mainly two major paradigms at work: linear logic and modal logic. The combination of approaches and pointers for further integration also suggests a grander vision for the field.
Author(s): Ruy J.G.B. de Queiroz (ed.)
Series: Trends in Logic 18
Publisher: Springer
Year: 2003
Language: English
Pages: 308
Contents......Page 6
List of Figures......Page 12
List of Tables......Page 16
Foreword......Page 18
Preface......Page 20
Contributing Authors......Page 22
Part I From a Structural Perspective......Page 24
1 Geometry of Deduction via Graphs of Proofs......Page 26
1 Motivation......Page 27
2 The idea of studying proofs as geometric objects......Page 35
3 Proof-nets......Page 40
4 Logical flow graphs......Page 57
5 Multiple-conclusion classical calculi......Page 73
6 Finale......Page 93
1 Preface......Page 112
2 The trip translation......Page 116
3 Chu’s construction......Page 121
4 Proof-nets, trips and translations......Page 123
3 Two Paradigms of Logical Computation in Affine Logic?......Page 134
1 Introduction......Page 135
2 Sequent calculus of MAL + Mix......Page 142
3 Additive mix......Page 146
4 Proof-nets for MAL + Mix......Page 149
5 Cut-elimination modulo irrelevance......Page 161
6 Symmetric reductions require Mix......Page 164
4 Proof Systems for π-Calculus Logics......Page 168
1 Introduction......Page 169
2 Preliminaries on the π-calculus......Page 171
3 A π-μ-calculus......Page 176
4 Example specifications......Page 182
5 Proof system, modal fragment......Page 185
6 Soundness and completeness for the modal fragment......Page 202
7 Proof rules for recursive formulas......Page 203
8 Finite control completeness......Page 211
9 Natural numbers......Page 215
10 Buffers......Page 217
11 Conclusion......Page 219
Part II From a Descriptive Perspective......Page 236
1 Introduction......Page 238
2 Kripke structures......Page 239
3 Temporal logic model checking......Page 241
4 Symbolic model checking......Page 248
5 Conclusion......Page 256
1 Introduction......Page 262
2 Finite directed graphs......Page 264
3 Finite acyclic directed graphs......Page 267
5 Loopless undirected graphs......Page 280
6 Modal definability......Page 281
7 κ-Colourable graphs......Page 284
8 Conclusions......Page 289
1 Introduction......Page 292
2 Background......Page 293
3 Caucal’s hierarchy......Page 297
4 Richer logics......Page 299
5 Finite model theory......Page 301
