Fork Algebras in Algebra, Logic and Computer Science

Contents......Page 10
Preface......Page 8
1.1 Software Specification Binary Relations and Fork......Page 13
2.1 History and Definitions......Page 17
2.2 Arithmetical Properties......Page 24
3.1 On the Origin of Fork Algebras......Page 31
3.2 Definition of the Classes......Page 33
3.3 Arithmetical Properties......Page 38
Chapter 4 Representability and Independence......Page 49
4.1 Representability of Abstract Fork Algebras......Page 50
4.2 Independence of the Axiomatization of Fork......Page 55
5.1 Basic Definitions......Page 61
5.2 Interpreting FOLE......Page 63
Chapter 6 Algebraization of Non-Classical Logics......Page 85
6.1 Basic Definitions and Properties......Page 87
6.2 The Fork Logic FL......Page 88
6.3 Modal Logics......Page 90
6.4 Representation of Constraints in FL......Page 92
6.5 Interpretability of Modal Logics in FL......Page 93
6.6 A Proof Theoretical Approach......Page 98
6.7 Interpretability of Propositional Dynamic Logic in FL......Page 103
6.8.2 Semantics of FL'......Page 114
6.9 A Rasiowa-Sikorski Calculus for FL'......Page 116
6.9.1 The Deduction System for FL'......Page 117
6.9.2 Soundness and Completeness of the Calculus FLC......Page 119
6.9.3 Examples of Proofs in the Calculus FLC......Page 124
6.10.1 Intuitionistic Logic......Page 127
6.10.2 Interpretability of Intuitionistic Logic in FL'......Page 129
6.10.3 A Fork Logic Calculus for Intuitionistic Logic......Page 133
6.10.3.1 Example......Page 136
6.11 A Relational Proof System for Minimal Intuitionistic Logic......Page 138
6.12.1 Method 1......Page 144
6.12.2 Method 2......Page 145
6.12.3 Method 3......Page 149
7.1 Introduction......Page 151
7.2 Filters and Sets......Page 153
7.3 The Relational Implication......Page 155
7.4 Representability and Expressiveness in Program Construction......Page 161
7.5 A Methodology for Program Construction......Page 162
7.6 Examples......Page 170
7.6.1 First Example......Page 171
7.6.1.1 Finding the Minimum Element in a List......Page 179
7.6.1.2 Finding the Minimum Common Ancestor......Page 180
7.6.2 Second Example......Page 186
7.6.2.1 Finding the Contiguous Sublists of Maximum Sum......Page 196
7.6.2.2 Finding the Longest Plateau......Page 199
7.7 A D&C Algorithm for MAXSTA......Page 204
7.8 Comparison with Previous Work......Page 215
Bibliography......Page 219
Index......Page 227