Computing and Software 734
Formalized Mathematics
Winter 2008

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. I. Lakatos, Proofs and Refutations, Cambridge University Press, 1976.
  5. Biographical Sketch of I. Lakatos.
  6. A. N. Whitehead and B. Russell, Principia Mathematica, Cambridge University Press, 1910–1913.

02 Review of Mathematical Logic

  1. P. B. Andrews, "A Reduction of the Axioms for the Theory of Propositional Types", Fundamenta Mathematicae, 52:345–350, 1963.
  2. P. B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Kluwer, 2002.
  3. B. Russell, "Mathematical Logic as Based on the Theory of types", American Journal of Mathematics, 30:222–262, 1908.
  4. A. Church, "A formulation of the simple theory of types", Journal of Symbolic Logic, 5:56–68, 1940.
  5. W. M. Farmer, "A basic extended simple type theory", SQRL Report No. 14, 12 pp., McMaster University, 2003 (revised 2004). PostScript PDF
  6. W. M. Farmer, "The seven virtues of simple type theory", forthcoming. doi:10.1016/j.jal.2007.11.001 PostScript PDF
  7. L. Henkin, "Completeness in the Theory of Types", Journal of Symbolic Logic, 15:81–91, 1950.
  8. L. Henkin, "A Theory of Propositional Types", Fundamenta Mathematicae, 52:323–344, 1963.

03 Theory Development Techniques

  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. W. M. Farmer, "A general method for safely overwriting theories in mechanized mathematics systems", Technical Report, 21 pp., The MITRE Corporation, 1994. PostScript PDF
  5. 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
  6. Noneuclidean Geometry.

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
  4. W. M. Farmer, "IMPS", in: F. Wiedijk, ed., The Seventeen Provers of the World, LNCS, 3600:72–87, 2006.
  5. 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.

05 Other 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, ed., The Seventeen Provers of the World, LNCS, 3600:72–87, 2006. 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. ProofPower suite of of specification and proof tools.
  25. PVS specification and verification system.
  26. RRL Rewrite Rule Laboratory.
  27. Theorema theorem prover.
  28. TPS Theorem Proving System.

06 Practise-Oriented Logics

  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, "Reasoning about partial functions with the aid of a computer", Erkenntnis, 43:279–294, 1995.
  3. W. M. Farmer and J. D. Guttman, "A set theory with support for partial functions, Studia Logica, 66:59–78, 2000. PostScript PDF
  4. W. M. Farmer, "STMM: A Set Theory for Mechanized Mathematics", Journal of Automated Reasoning, 26:269–289, 2001. PostScript PDF
  5. W. M. Farmer, "Formalizing undefinedness arising in calculus", in: D. Basin and M. Rusinowitch, eds., Automated Reasoning, LNCS, 3097:475–489, 2004. PostScript PDF
  6. W. M. Farmer, "Chiron: A multi-paradigm logic", in: R. Matuszewski and A. Zalewska, eds, From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric, 10(23):1–19, 2007. PostScript PDF

07 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. D. Sannella and A. Tarlecki, "Towards formal development of programs from algebraic specifications: Implementations revisited", Acta Informatica, 25:233–281, 1988.
  9. D. Smith and M. Lowry, "Algorithmic theories and design tactics", Science of Computer Programming, 14:305–321, 1990
  10. W. Turski and T. Maibaum, The Specification of Computer Programs, Addison-Wesley, 1987.