Computing and Software 734
Formalized Mathematics
Winter 2005

Instructor: William M. Farmer

References

01 What is Formalized Mathematics?

  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
  2. W. M. Farmer and M. v. Mohrenschildt, in: B. Buchberger, G. Gonnet, and M. Hazewinkel, eds, Mathematical Knowledge Management, special issue of Annals of Mathematics and Artificial Intelligence, 38:165-191, 2003. PostScript PDF
  3. Formal Methods Web site.
  4. A. N. Whitehead and B. Russell, Principia Mathematica, Cambridge University Press, 1910-1913.

02 The Axiomatic Method

  1. N. Bourbaki, Eléments de mathématique, mid 1900s.
  2. D. M. Bressoud, Proofs and Confirmations: The Story of the Alternating-Sign Matrix Conjecture, Cambridge University Press, 1999.
  3. Euclid, The Elements, 300 BC.
  4. I. Lakatos, Proofs and Refutations, Cambridge University Press, 1976.
  5. Biographical Sketch of I. Lakatos.

03 Interactive Theorem Proving Systems

  1. F. Wiedijk, "Comparing mathematical provers", in: A. Asperti, B. Buchberger, and J. Davenport, eds., Mathematical Knowledge Management, LNCS, 2594:188-202, 2003. PostScript PDF
  2. F. Wiedijk, "The sixteen provers of the world". PostScript PDF
  3. ACL2 (A Computational Logic for Applicative Common Lisp).
  4. Alfa proof editor.
  5. Automath.
  6. Coq proof assistant.
  7. Ergo interactive proof tool.
  8. EVES tool.
  9. HOL (Higher Order Logic) theorem prover.
  10. IMPS Interactive Mathematical Proof System.
  11. INKA inductive theorem prover.
  12. Isabelle generic theorem prover.
  13. Jape (Just Another Proof Editor).
  14. LCF.
  15. LEGO proof assistant.
  16. LP (Larch Prover).
  17. Metamath Proof Explorer.
  18. Mizar tool.
  19. Nqthm (Boyer-Moore prover).
  20. Nuprl tool.
  21. Omega theorem proving system.
  22. Otter automated deduction system tool.
  23. PhoX proof assistant.
  24. PVS specification and verification system.
  25. RRL Rewrite Rule Laboratory.
  26. Theorema theorem prover.
  27. TPS Theorem Proving System.

04 The IMPS Interactive Mathematical Proof System

  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 Styles of Formal Proof

  1. W. M. Farmer, J. D. Guttman, M. E. Nadel, and F. J. Thayer, "Proof script pragmatics in IMPS", in: A. Bundy, ed., Automated Deduction--CADE-12, LNCS, 814: 356-370, 1994.

06 Practice-Oriented Logics

  1. P. B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Kluwer, 2002.
  2. A. Church, "A formulation of the simple theory of types", Journal of Symbolic Logic, 5:56-68, 1940.
  3. W. M. Farmer, "A partial functions version of Church's simple theory of types", Journal of Symbolic Logic, 55:1269-1291, 1990.
  4. W. M. Farmer, "Reasoning about partial functions with the aid of a computer", Erkenntnis, 43:279-294, 1995.
  5. W. M. Farmer and J. D. Guttman, "A set theory with support for partial functions, Studia Logica, 66:59-78, 2000. PostScript PDF
  6. W. M. Farmer, "STMM: A Set Theory for Mechanized Mathematics", Journal of Automated Reasoning, 26:269-289, 2001. PostScript PDF
  7. W. M. Farmer, "A basic extended simple type theory", SQRL Report No. 14, 12 pp., McMaster University, 2004. PostScript PDF
  8. W. M. Farmer, "Formalizing undefinedness arising in calculus", in: D. Basin and M. Rusinowitch, eds., Automated Reasoning, LNCS, 3097:475-489, 2004.
  9. W. M. Farmer, "The seven virtues of simple type theory", SQRL Report No. 18, 27 pp., McMaster University, 2004. PostScript PDF

07 Definition and Specification Principles

  1. W. M. Farmer, "A general method for safely overwriting theories in mechanized mathematics systems", Technical Report, 21 pp., The MITRE Corporation, 1994. PostScript PDF
  2. W. M. Farmer, "A scheme for defining partial higher-order functions by recursion", In: A. Butterfield, ed., 3rd Irish Workshop on Formal Methods, 13 pp., electronic Workshops in Computing, Springer-Verlag, 1999. PostScript PDF

08 The Little Theories Method

  1. J. Barwise and J. Seligman, Information Flow : The Logic of Distributed Systems, Cambridge University Press, 1997.
  2. 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.
  3. 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
  4. 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
  5. W. M. Farmer, "An infrastructure for intertheory reasoning", in: In: D. McAllester, ed., Automated Deduction--CADE-17, LNCS, 1831:115-131, 2000. PostScript PDF
  6. J. Carette, W. M. Farmer, and J. Wajs, "Trustable communication between mathematics systems", Technical Report, 22 pp., McMaster University, 2004. (This is a longer, revised version of the paper with the same name published in the proceedings of Calculemus 2003.) 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.

09 Symbolic Computation in Formal Proofs

  1. W. M. Farmer, J. D. Guttman, and F. J. Thayer, "Contexts in mathematical reasoning and computation", Journal of Symbolic Computation, 19:201-216, 1995.