Computer Science 773
Formalized Mathematics
Winter 2002

Instructor: William M. Farmer


References

Theorem Proving Systems

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

02 What is Mathematics?

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

03 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.

04 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

05 Alternative Logics

  1. P. B. Andrews, "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof", Academic Press, 1986.
  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, "STMM: a Set Theory for Mechanized Mathematics, Journal of Automated Reasoning, 26:269-289, 2001. PostScript PDF
  5. W. M. Farmer and J. D. Guttman, "A set theory with support for partial functions, Studia Logica, 66:59-78, 2000. PostScript PDF

06 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

07 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

08 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.

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.