Introduction 1
Ⅰ Propositional Logic 7
1 Orders and Trees 7
2 Propositions,Connectives and Truth Tables 12
3 Truth Assignments and Valuations 23
4 Tableau Proofs in Propositional Calculus 27
5 Soundness and Completeness of Tableau Proofs 38
6 Deductions from Premises and Compactness 40
7 An Axiomatic Approach 47
8 Resolution 49
9 Refining Resolution 62
10 Linear Resolution,Horn Clauses and PROLOG 66
Ⅱ Predicate Logic 81
1 Predicates and Quantifiers 81
2 The Language：Terms and Formulas 83
3 Formation Trees，Structures and Lists 89
4 Semantics：Meaning and Truth 95
5 Interpretations of PROLOG Programs 100
6 Proofs：Complete Systematic Tableaux 108
7 Soundness and Completeness of Tableau Proofs 120
8 An Axiomatic Approach 127
9 Prenex Normsl Form and Skolemization 128
10 Herbrand’s Theorem 133
11 Unification 137
12 The Unification Algorithm 141
13 Resolution 145
14 Refining Resolution：Linear Resolution 153
Ⅲ PROLOG 159
1 SLD-Resolution 159
2 Implementations：Searching and Backtracking 166
3 Controlling the Implementation：Cut 178
4 Termination Conditions for PROLOG Programs 182
5 Equality 188
6 Negation as Failure 192
7 Negation and Nonmonotonic Logic 203
8 Computability and Undecidability 211
Ⅳ Modal Logic 221
1 Possibility and Necessity：Knowledge or Belief 221
2 Frames and Forcing 224
3 Modal Tableaux 228
4 Soundness and Completeness 239
5 Modal Axioms and Special Accessibility Relations 249
6 An Axiomatic Approach 259
Ⅴ Intuitionistic Logic 263
1 Intuitionism and Constructivism 263
2 Frames and Forcing 265
3 Intuitionistic Tableaux 275
4 Soundness and Completeness 285
5 Decidability and Undecidability 293
6 A Comparative Guide 306
Ⅵ Elements of Set Theory 315
1 Some Basic Axioms of Set Theory 315
2 Boole’8 Algebra of Sets 318
3 Relations．Functions and the Power Set Axiom 321
4 The Natural Numbers，Arithmetic and Infinity 328
5 Replacement．Choice and Foundation 339
6 Zermelo-Fraenkel Set Theory in Predicate Logic 345
7 Cardinality：Finite and Countable 348
8 Ordinal Numbers 354
9 Ordinal Arithmetic and Transfinite Induction 360
10 Transfinite Recursion，Choice and the Ranked Universe 364
11 Cardinals and Cardinal Arithmetic 368
Appendix A：An Historical Overview 375
1 Calculus 375
2 Logic 376
3 Leibniz’8 Dream 379
4 Nineteenth Century Logic 380
5 Nineteenth Century Foundatlons of Mathematics 383
6 Twentieth Century Foundations of Mathematics 387
7 Early Twentieth Century Logic 389
8 Deduction and Computation 392
9 Recent Automation of Logic and PROLOG 395
10 The Future 395
Appendix B：A Genealogical Database 399
Bibliography 409
Index of Symbols 439
Index ofTerms 443