Mathematics and Its Applications

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 theorem-proving [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 satisfiability case.- 9.5 A proof procedure for the predicate calculus.- 9.6 Remarks on mathematical disciplines.- Three. Decidability and Complexity.- 10. Games, Logic and Computers [1965a].- Appendix: Notes on a Class of Tiling Problems [1975(60)].- 11. Dominoes and the AEA Case of the Decision Problem [1963(62)].- 12. Towards Feasible Solutions of the Tautology Problem (with B.Dunhan) [1976(74)].- 12.1 Computational complexity and Boolean validity.- 12.2 A brief overview with some general observations.- 12.3 Some basic properties of Boolean validity.- 12.4 Some calculations and classifications.- 12.5 Hard examples and negative results.- 12.6 A feasible decision procedure for biconditional expressions.- 12.7 Two partial methods and an indication of two generic methods.- 13. Ranked Matching and Hospital Interns (with D.A.Martin) [(1977)].- 13.1 Preliminary.- 13.2 Deletion of useless names: Operations I and II.- 13.3 The canonical form T1 of T.- 13.4 The student and hospital optimal assignments.- 13.5 Mixed assignments and a characterization of all stable assignments.- 13.6 The marriage problem.- Four. Topics from Theory to Practice.- 14. Logical Fragments Relevant to Computer Science.- 14.1 Logic of many-sorted theories [1952(50)].- 14.2 Ackermann's consistency proof [1962(53)].- 14.3 Partial systems of number theory [1962(55)].- 14.4 The calculus of partial predicates and its extension to set theory [1961(61)].- 14.5 Model theory [1974(71)].- 15. Computers and Mathematical Activity.- 15.1 Remarks on machines, sets and the decision problem [1964(63)].- 15.2 Logic and computers [1965].- 15.3 Remarks on mathematics and computers [1970(67)].- 15.4 On the long-range prospects of automatic theorem-proving [1970(68)a].- 16. On Information Processing of the Chinese Language [1979].- The List of the Publications of the Author.