Computer Science 773
Formalized Mathematics
Winter 2001

Instructor: William M. Farmer

References

Theorem Proving Systems

  1. ACL2 (A Computational Logic for Applicative Common Lisp).
  2. Coq proof assistant.
  3. Ergo interactive proof tool.
  4. EVES tool.
  5. HOL (Higher Order Logic) theorem prover.
  6. IMPS Interactive Mathematical Proof System.
  7. Isabelle generic theorem prover.
  8. Jape (Just Another Proof Editor).
  9. LP (Larch Prover).
  10. LEGO proof assistant.
  11. Metamath Proof Explorer.
  12. Mizar tool.
  13. Nqthm (Boyer-Moore prover).
  14. Nuprl tool.
  15. Otter automated deduction system tool.
  16. PVS specification and verification system.
  17. RRL Rewrite Rule Laboratory.
  18. TPS Theorem Proving System.

01 What is Mathematics?

  1. Imre Lakatos, Proofs and Refutations, Cambridge University Press, 1976.
  2. Biographical Sketch of I. Lakatos.

02 The Axiomatic Method

  1. J. Barwise and J. Seligman, Information Flow : The Logic of Distributed Systems, Cambridge University Press, 1997.
  2. N. Bourbaki, Eléments de mathématique, mid 1900s.
  3. R. Burstall and J. Goguen, "Putting theories together to make specifications", Proceedings of the Fifth International Joint Conference on Artificial Intelligence, pp. 1045-1058, 1977.
  4. Euclid, The Elements, 300 BC.
  5. W. M. Farmer, "Theory interpretation in simple type theory", in: J. Heering et al., eds., Higher-Order Algebra, Logic, and Term Rewriting, LNCS, 816:96-123, 1994. PostScript PDF
  6. W. M. Farmer, J. D. Guttman, and F. J. Thayer, "Little theories", in: D. Kapur, ed., Automated Deduction--CADE-11, LNCS, 607:567-581, 1992. PostScript PDF
  7. R. Nakajima and T. Yuasa (eds.), The IOTA Programming System, LNCS, Vol. 160, 1982.
  8. Noneuclidean Geometry.
  9. D. Sannella and A. Tarlecki, "Towards formal development of programs from algebraic specifications: Implementations revisited", Acta Informatica, 25:233-281, 1988.
  10. D. Smith and M. Lowry, "Algorithmic theories and design tactics", Science of Computer Programming, 14:305-321, 1990
  11. W. Turski and T. Maibaum, The Specification of Computer Programs, Addison-Wesley, 1987.
  12. A. N. Whitehead and B. Russell, Principia Mathematica, Cambridge University Press, 1910-1913.

03 Mechanized Mathematics Systems

  1. W. M. Farmer, "A proposal for the development of an interactive mathematics laboratory for mathematics education", in: E. Melis, ed., Proceedings of the Workshop on Deduction Systems for Mathematics Education, pp. 20-25, CADE-17, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 16, 2000. PostScript PDF

04 Introduction to IMPS

  1. W. M. Farmer, J. D. Guttman, and F. J. Thayer, "IMPS: an Interactive Mathematical Proof System", Journal of Automated Reasoning, 11:213-248, 1993. PostScript PDF
  2. W. M. Farmer, J. D. Guttman, and F. J. Thayer, "The IMPS user's manual", Technical Report M-93B138, 289 pp., The MITRE Corporation, November 1993. HTML PostScript PDF
  3. W. M. Farmer, J. D. Guttman, and F. J. Thayer Fábrega, "IMPS: an updated system description", in: M. McRobbie and J. Slaney, eds., Automated Deduction--CADE-13, LNCS, 1104:298-302, 1996. PostScript PDF

05 Review of Logic

  1. C. C. Chang and H. J. Keisler, Model Theory, North Holland, 1990.
  2. H. B. Enderton, A Mathematical Introduction to Logic, Academic Press, 1972.

06 What is Missing from First-Order Logic?

  1. W. M. Farmer, "A partial functions version of Church's simple theory of types", Journal of Symbolic Logic, 55:1269-1291, 1990.
  2. W. M. Farmer, "STMM: a Set Theory for Mechanized Mathematics, Journal of Automated Reasoning, 26:269-289, 2001. PostScript PDF
  3. W. M. Farmer and J. D. Guttman, "A set theory with support for partial functions, Studia Logica, 66:59-78, 2000. PostScript PDF

07 Higher-Order Logic

  1. A. Church, "A formulation of the simple theory of types", Journal of Symbolic Logic, 5:56-68, 1940.
  2. P. B. Andrews, "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof", Academic Press, 1986.
  3. W. M. Farmer, "A partial functions version of Church's simple theory of types", Journal of Symbolic Logic, 55:1269-1291, 1990.

08 Set Theory

  1. W. M. Farmer, "STMM: a Set Theory for Mechanized Mathematics, Journal of Automated Reasoning, 26:269-289, 2001. PostScript PDF
  2. W. M. Farmer and J. D. Guttman, "A set theory with support for partial functions, Studia Logica, 66:59-78, 2000. PostScript PDF

09 Theory Development

  1. W. M. Farmer, "An infrastructure for intertheory reasoning", in: In: D. McAllester, ed., Automated Deduction--CADE-17, LNCS, 1831:115-131, 2000. PostScript PDF

Miscellaneous References

  1. Formal Methods.