Elementary Logic with Applications: A Procedural Perspective for Computer Scientists

Title ......Page 3
Copyright ......Page 4
Contents ......Page 5
Preface ......Page 9
Introduction ......Page 13
1 Propositional logic ......Page 15
1.1 Introducing classical propositional logic ......Page 17
1.1.1 Formal language ......Page 18
1.1.2 Computing truth tables ......Page 22
1.2 Notions of truth and validity ......Page 26
1.2.1 Equivalences ......Page 27
1.2.2 Arguments and consequence relations ......Page 30
1.3 Worked examples ......Page 37
2 Some non-classical logics ......Page 53
2.1 Many-valued logics ......Page 54
2.2.1 Temporal logic ......Page 57
2.2.2 Intuitionistic logic ......Page 60
2.2.3 Resource logics ......Page 62
2.3 Another look at intuitionistic logic ......Page 64
2.4 Worked examples ......Page 68
3 Introducing forward rules ......Page 83
3.1.1 Rules for conjunction ......Page 86
3.1.2 Rules for disjunction ......Page 87
3.1.3 Rules for implication ......Page 88
3.1.4 Rules for negation ......Page 89
3.2 Using subcomputations ......Page 91
3.3 Example proofs ......Page 95
3.3.1 Proofs using A, V and —> rules ......Page 96
3.3.2 Proofs involving negation rules ......Page 98
3.4 Formal descriptions of proofs ......Page 103
4 From forward to backward rules ......Page 109
4.1 Introductory heuristics ......Page 110
4.1.1 Adding positive and negative assumptions ......Page 111
4.1.2 Restart rule ......Page 117
4.1.3 A heuristic for negation ......Page 119
4.1.4 Rewriting assumptions ......Page 120
4.1.5 Summary of computation rules ......Page 123
4.2 Worked examples ......Page 124
4.3 A deterministic goal-directed algorithm ......Page 136
5 Methodology and metatheorems ......Page 143
5.1 Consequence relations and Hilbert systems ......Page 144
5.2 Hilbert formulation of a logic ......Page 146
5.3 Metatheorems about classical logic consequence ......Page 150
5.4 Prepositional soundness and completeness ......Page 152
5.5 Proof of soundness ......Page 156
5.6 Proof of completeness ......Page 157
5.7 Fragment of {A, ->, L} ......Page 169
5.9 Worked examples ......Page 172
6 Introducing predicate logic ......Page 181
6.1 Simple sentences ......Page 182
6.1.1 Building simple sentences ......Page 183
6.1.2 Truth of simple sentences ......Page 185
6.2 Variables and quantifiers ......Page 187
6.2.1 Scope of quantifiers ......Page 190
6.2.2 Quantifier rules and equivalences ......Page 192
6.2.3 Prenex normal form ......Page 196
6.3 Formal definitions ......Page 198
6.4 Worked examples ......Page 203
7 Forward and backward predicate rules ......Page 219
7.1 Reasoning with variables ......Page 220
7.1.1 Introduction to unification ......Page 224
7.1.2 A unification algorithm ......Page 226
7.1.3 The meaning of variables in clauses ......Page 229
7.1.4 Skolemization ......Page 231
7.2 Reasoning forwards ......Page 235
7.3 Reasoning backward ......Page 241
7.3.1 Connection with resolution ......Page 249
7.4 Decidability ......Page 251
7.5 Worked examples ......Page 252
8.1 Getting started with PROLOG\'S syntax ......Page 257
8.2 Trying it all out ......Page 262
8.3 PROLOG\'S strategy for proving goals ......Page 267
8.4 Working with Lists ......Page 270
8.4.1 Terminology and Notation ......Page 271
8.4.2 Unifying lists ......Page 272
8.4.3 Useful predicates about lists ......Page 273
8.5 Operators in PROLOG ......Page 275
8.5.1 Operator Precedence and Associativity ......Page 276
8.5.2 Some built-in PROLOG operators ......Page 277
8.5.3 Declaring your own operators ......Page 281
8.6 Backtracking ......Page 282
8.7 Cut ......Page 284
8.8 PROLOG and classical logic ......Page 286
8.9 Clauses as first-order logic formulae ......Page 287
8.10 Theorem proving in PROLOG ......Page 290
8.11 From PROLOG to classical logic ......Page 292
Answers to the exercises ......Page 295
Bibliography ......Page 349
Index ......Page 357