Preface |
|
vii | |
|
Introduction and Motivations |
|
|
1 | (4) |
|
Software Specification, Binary Relations and Fork |
|
|
1 | (4) |
|
Algebras of Binary Relations and Relation Algebras |
|
|
5 | (14) |
|
|
5 | (7) |
|
|
12 | (7) |
|
Proper and Abstract Fork Algebras |
|
|
19 | (18) |
|
On the Origin of Fork Algebras |
|
|
19 | (2) |
|
Definition of the Classes |
|
|
21 | (5) |
|
|
26 | (11) |
|
Representability and Independence |
|
|
37 | (12) |
|
Representability of Abstract Fork Algebras |
|
|
38 | (5) |
|
Independence of the Axiomatization of Fork |
|
|
43 | (6) |
|
Interpretability of Classical First-Order Logic |
|
|
49 | (24) |
|
|
49 | (2) |
|
|
51 | (22) |
|
Algebraization of Non-Classical Logics |
|
|
73 | (66) |
|
Basic Definitions and Properties |
|
|
75 | (1) |
|
|
76 | (2) |
|
|
78 | (2) |
|
Representation of Constraints in FL |
|
|
80 | (1) |
|
Interpretability of Modal Logics in FL |
|
|
81 | (5) |
|
A Proof Theoretical Approach |
|
|
86 | (5) |
|
Interpretability of Propositional Dynamic Logic in FL |
|
|
91 | (11) |
|
|
102 | (2) |
|
|
102 | (1) |
|
|
102 | (2) |
|
A Rasiowa--Sikorski Calculus for FL' |
|
|
104 | (11) |
|
The Deduction System for FL' |
|
|
105 | (2) |
|
Soundness and Completeness of the Calculus FLC |
|
|
107 | (5) |
|
Examples of Proofs in the Calculus FLC |
|
|
112 | (3) |
|
A Relational Proof System for Intuitionistic Logic |
|
|
115 | (11) |
|
|
115 | (2) |
|
Interpretability of Intuitionistic Logic in FL' |
|
|
117 | (4) |
|
A Fork Logic Calculus for Intuitionistic Logic |
|
|
121 | (3) |
|
|
124 | (2) |
|
A Relational Proof System for Minimal Intuitionistic Logic |
|
|
126 | (6) |
|
Relational Reasoning in Intermediate Logics |
|
|
132 | (7) |
|
|
132 | (1) |
|
|
133 | (4) |
|
|
137 | (2) |
|
A Calculus for Program Construction |
|
|
139 | (68) |
|
|
139 | (2) |
|
|
141 | (2) |
|
The Relational Implication |
|
|
143 | (6) |
|
Representability and Expressiveness in Program Construction |
|
|
149 | (1) |
|
A Methodology for Program Construction |
|
|
150 | (8) |
|
|
158 | (34) |
|
|
159 | (8) |
|
Finding the Minimum Element in a List |
|
|
167 | (1) |
|
Finding the Minimum Common Ancestor |
|
|
168 | (6) |
|
|
174 | (10) |
|
Finding the Contiguous Sublists of Maximum Sum |
|
|
184 | (3) |
|
Finding the Longest Plateau |
|
|
187 | (5) |
|
A D&C Algorithm for MAXSTA |
|
|
192 | (11) |
|
Comparison with Previous Work |
|
|
203 | (4) |
Bibliography |
|
207 | (8) |
Index |
|
215 | |