From Logic Programming to Prolog

List of Figures......Page 9
List of Programs......Page 11
Preface......Page 13
Acknowledgements......Page 15
1.1 Background......Page 17
1.2 Declarative Programming......Page 18
1.3 Logic Programming Paradigm......Page 19
1.4 Shortcomings of Prolog......Page 24
1.5 Theoretical Foundations of Logic Programming......Page 27
1.6 Program Verification......Page 28
1.7 Prolog and Program Verification......Page 29
1.8 Structure of the Book......Page 30
1.9 Further Reading......Page 32
1.10 References......Page 33
2.1 Terms......Page 34
2.2 Substitutions......Page 36
2.3 Unifiers......Page 40
2.4 * The Nondeterministic Robinson Algorithm......Page 42
2.5 * Robinson’s Algorithm......Page 46
2.6 The Martelli–Montanari Algorithm......Page 47
2.7 Properties of Mgus......Page 53
2.8 Concluding Remarks......Page 56
2.10 Summary......Page 57
2.11 References......Page 58
3 Logic Programs: Procedural Interpretation......Page 60
3.1 Queries and Programs......Page 61
3.2 SLD-derivations......Page 62
3.3 Comparison with other Programming Styles......Page 67
3.4 Resultants......Page 68
3.5 Properties of SLD-derivations......Page 72
3.6 * SLD-derivations with Idempotent Mgus......Page 76
3.7 Selection Rules......Page 79
3.8 SLD-trees......Page 83
3.9 Concluding Remarks......Page 87
3.10 Bibliographic Remarks......Page 88
3.12 References......Page 89
4 Logic Programs: Declarative Interpretation......Page 91
4.1 Algebras......Page 92
4.2 Interpretations......Page 93
4.3 Soundness of the SLD-resolution......Page 95
4.4 Term Interpretations......Page 97
4.5 Completeness of the SLD-resolution......Page 100
4.6 * Least Term Models......Page 103
4.7 Operators and their Fixpoints......Page 105
4.8 * Least Term Models, continued......Page 107
4.9 Herbrand Interpretations......Page 108
4.10 Least Herbrand Models......Page 111
4.11 * Comparison of the Least Term and the Least Herbrand Models......Page 115
4.12 Concluding Remarks......Page 116
4.15 References......Page 118
5 Programming in Pure Prolog......Page 120
5.1 Introduction......Page 121
5.2 The Empty Domain......Page 130
5.3 Finite Domains......Page 131
5.4 Numerals......Page 134
5.5 Lists......Page 139
5.6 Complex Domains......Page 152
5.7 Binary Trees......Page 154
5.8 Concluding Remarks......Page 157
5.11 References......Page 160
6 Termination......Page 162
6.1 Multiset Ordering......Page 163
6.2 Terminating Programs......Page 165
6.3 Applications......Page 168
6.4 * Characterizing Terminating Programs......Page 171
6.5 Left Terminating Programs......Page 173
6.6 Applications......Page 179
6.7 * Characterizing Left Terminating Programs......Page 182
6.8 * An Improvement......Page 185
6.9 Concluding Remarks......Page 189
6.10 Bibliographic Remarks......Page 190
6.11 Summary......Page 191
6.12 References......Page 192
7 The Occur-check Problem......Page 194
7.1 Occur-check Free Programs......Page 195
7.2 NSTO Lemma......Page 196
7.3 Well-moded Queries and Programs......Page 199
7.4 Occur-check Freedom via Well-modedness......Page 205
7.5 Nicely Moded Programs......Page 209
7.6 Occur-check Freedom via Nice Modedness......Page 211
7.7 * Unfolding......Page 214
7.8 * Insertion of the Occur-checks......Page 216
7.9 Concluding Remarks......Page 218
7.10 Bibliographic Remarks......Page 219
7.12 References......Page 220
8.1 Introduction......Page 223
8.2 Well-asserted Queries and Programs......Page 225
8.3 Applications......Page 229
8.4 Computing Strongest Postconditions......Page 235
8.5 Applications......Page 240
8.6 Absence of Failures......Page 242
8.7 Concluding Remarks......Page 243
8.8 Bibliographic Remarks......Page 245
8.10 References......Page 246
9 Programming in Pure Prolog with Arithmetic......Page 248
9.1 Operators......Page 249
9.2 Arithmetic Comparison Relations......Page 252
9.3 Complex Domains......Page 254
9.4 Lists of Integers......Page 256
9.5 Difference Lists......Page 259
9.6 Binary Search Trees......Page 262
9.7 Evaluation of Arithmetic Expressions......Page 266
9.8 Concluding Remarks......Page 269
9.9 Bibliographic Remarks......Page 270
9.11 References......Page 271
10.1 Syntax......Page 273
10.2 Procedural Interpretation......Page 274
10.3 Termination......Page 275
10.4 Occur-check Freedom......Page 279
10.5 Well-typed Queries and Programs......Page 280
10.6 Absence of Run-time Errors......Page 286
10.7 Partial Correctness......Page 288
10.8 Concluding Remarks......Page 294
10.9 Bibliographic Remarks......Page 295
10.11 References......Page 296
11 Towards Full Prolog......Page 298
11.1 Cut......Page 299
11.2 Sets......Page 304
11.3 Collecting All Solutions......Page 307
11.4 Meta-variables......Page 309
11.5 Negation......Page 311
11.6 Directed Graphs......Page 314
11.7 Non-monotonic Reasoning......Page 318
11.8 Term Inspection Facilities......Page 321
11.9 Program Manipulation Facilities......Page 325
11.10 Input/Output Facilities......Page 328
11.11 Concluding Remarks......Page 330
11.12 Bibliographic Remarks......Page 332
11.13 Summary......Page 333
11.14 References......Page 334
Index......Page 338