One. Broad Issues.- 1. On Formalization.- 1.1 Systematization [1955(53)].- 1.2 Communication.- 1.3 Clarity and consolidation.- 1.4 Rigour.- 1.5 Approximation to intuition.- 1.6 Application to philosophy.- 1.7 Too many digits.- 1.8 Ideal language.- 1.9 How artificial language?.- 1.10 The paradoxes.- 2. The Concept of Computability [(1953)].- 2.1 Formalizing intuitive concepts.- 2.2 The intuitive concept of computability.- 2.3 Computation by theoretical machines.- 2.4 General recursive functions.- 2.5 Constructive proofs.- 2.6 Effective methods.- 2.7 Speed functions.- 2.8 Transfinite recursions.- 2.9 The indeterminate domain of computable functions.- 3. Process and Existence in Mathematics [1961(60)].- 4. Logic, Computation and Philosophy [1971(66)].- 4.1 Logic and logical positivism.- 4.2 What is mathematics?.- 4.3 Logic and computation.- 4.4 Relatively undecidable propositions and absolutely unsolvable problems.- 4.5 Foundations of set theory.- 4.6 What is mathematics? (continued).- Two. Automated Theorem Proving(ATP).- 5. Computer Theorem Proving and Artificial Intelligence [1984(82)].- Appendix: Citation for Haowang as Winner of Milestone Award in Automatic Theorem-Proving.- 6. Proving Theorems by Pattern Recognition, I [1960(59)].- 6.1 Introduction.- 6.2 A program that does 9 chapters of Principia in 9 minutes.- 6.3 The E1A case solved with sequential tables.- 6.4 General remarks.- 7. Observations on ATP.- 7.1 Mechanical mathematics and inferential analysis [1963(61)].- 7.2 The mechanization of mechanical arguments [1963(62)a].- 7.3 Formalization and automatic theoremproving [1965(64)].- 8. Some Data for ATP.- 8.1 On axioms of conditional set existence [1967(66)].- 8.2 Natural hulls and set existence [1967(66)a].- 8.3 A theorem on definitions of the Zermelo-Neumann ordinals [1967(66)b].- 9. Proving Theorems by Pattern Recognition, II [1961(60)a].- 9.1 A survey of the decision problem.- 9.2 The Skolem, case.- 9.3 The A2E satisfiability case.- 9.4 The A1E1A1 satlC*