Introduction

Ⅰ Propositional Logic

1 Orders and Trees

2 Propositions,Connectives and Truth Tables

3 Truth Assignments and Valuations

4 Tableau Proofs in Propositional Calculus

5 Soundness and Completeness of Tableau Proofs

6 Deductions from Premises and Compactness

7 An Axiomatic Approach

8 Resolution

9 Refining Resolution

10 Linear Resolution,Horn Clauses and PROLOG

Ⅱ Predicate Logic

1 Predicates and Quantifiers

2 The Language：Terms and Formulas

3 Formation Trees，Structures and Lists

4 Semantics：Meaning and Truth

5 Interpretations of PROLOG Programs

6 Proofs：Complete Systematic Tableaux

7 Soundness and Completeness of Tableau Proofs

8 An Axiomatic Approach

9 Prenex Normsl Form and Skolemization

10 Herbrand’s Theorem

11 Unification

12 The Unification Algorithm

13 Resolution

14 Refining Resolution：Linear Resolution

Ⅲ PROLOG

1 SLD-Resolution

2 Implementations：Searching and Backtracking

3 Controlling the Implementation：Cut

4 Termination Conditions for PROLOG Programs

5 Equality

6 Negation as Failure

7 Negation and Nonmonotonic Logic

8 Computability and Undecidability

Ⅳ Modal Logic

1 Possibility and Necessity：Knowledge or Belief

2 Frames and Forcing

3 Modal Tableaux

4 Soundness and Completeness

5 Modal Axioms and Special Accessibility Relations

6 An Axiomatic Approach

Ⅴ Intuitionistic Logic

1 Intuitionism and Constructivism

2 Frames and Forcing

3 Intuitionistic Tableaux

4 Soundness and Completeness

5 Decidability and Undecidability

6 A Comparative Guide

Ⅵ Elements of Set Theory

1 Some Basic Axioms of Set Theory

2 Boole’8 Algebra of Sets

3 Relations．Functions and the Power Set Axiom

4 The Natural Numbers，Arithmetic and Infinity

5 Replacement．Choice and Foundation

6 Zermelo-Fraenkel Set Theory in Predicate Logic

7 Cardinality：Finite and Countable

8 Ordinal Numbers

9 Ordinal Arithmetic and Transfinite Induction

10 Transfinite Recursion，Choice and the Ranked Universe

11 Cardinals and Cardinal Arithmetic

Appendix A：An Historical Overview

1 Calculus

2 Logic

3 Leibniz’8 Dream

4 Nineteenth Century Logic

5 Nineteenth Century Foundatlons of Mathematics

6 Twentieth Century Foundations of Mathematics

7 Early Twentieth Century Logic

8 Deduction and Computation

9 Recent Automation of Logic and PROLOG

10 The Future

Appendix B：A Genealogical Database

Bibliography

Index of Symbols

Index ofTerms