Computer Science 773
Formalized Mathematics
Winter 2002
References
Theorem Proving Systems
- ACL2
(A Computational Logic for Applicative Common Lisp).
- Alfa proof
editor.
- Coq proof assistant.
-
Ergo interactive proof tool.
- EVES tool.
- HOL
(Higher Order Logic) theorem prover.
- IMPS Interactive
Mathematical Proof System.
- INKA inductive theorem prover.
- Isabelle
generic theorem prover.
- Jape
(Just Another Proof Editor).
- LEGO proof assistant.
- LP
(Larch Prover).
- Metamath
Proof Explorer.
- Mizar
tool.
- Nqthm
(Boyer-Moore prover).
- Nuprl
tool.
- Omega theorem
proving system.
- Otter automated
deduction system tool.
- PhoX
proof assistant.
- PVS specification and
verification system.
- RRL Rewrite
Rule Laboratory.
- Theorema theorem prover.
- TPS Theorem Proving System.
02 What is Mathematics?
- Imre Lakatos, Proofs and Refutations,
Cambridge University Press, 1976.
-
Biographical Sketch of I. Lakatos.
03 Review of Logic
- C. C. Chang and H. J. Keisler, Model Theory, North
Holland, 1990.
- H. B. Enderton, A Mathematical Introduction to
Logic, Academic Press, 1972.
04 What is Missing from First-Order Logic?
- W. M. Farmer, "A partial functions version of Church's simple
theory of types", Journal of Symbolic Logic,
55:1269-1291, 1990.
- W. M. Farmer, "STMM: a Set Theory for Mechanized Mathematics,
Journal of Automated Reasoning, 26:269-289, 2001. PostScript
PDF
- 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
- P. B. Andrews, "An Introduction to Mathematical Logic and
Type Theory: To Truth Through Proof", Academic Press, 1986.
- A. Church, "A formulation of the simple theory of types",
Journal of Symbolic Logic, 5:56-68, 1940.
- W. M. Farmer, "A partial functions version of Church's simple
theory of types", Journal of Symbolic Logic,
55:1269-1291, 1990.
- W. M. Farmer, "STMM: a Set Theory for Mechanized Mathematics,
Journal of Automated Reasoning, 26:269-289, 2001. PostScript
PDF
- 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
- 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
- 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
- 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
- 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
- J. Barwise and J. Seligman, Information Flow : The Logic
of Distributed Systems, Cambridge University Press, 1997.
- N. Bourbaki, Eléments de mathématique,
mid 1900s.
- 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.
- Euclid, The Elements, 300 BC.
- 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
- 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
- R. Nakajima and T. Yuasa (eds.), The IOTA Programming
System, LNCS, Vol. 160, 1982.
- Noneuclidean Geometry.
- D. Sannella and A. Tarlecki, "Towards formal development of
programs from algebraic specifications: Implementations
revisited", Acta Informatica, 25:233-281, 1988.
- D. Smith and M. Lowry, "Algorithmic theories and design
tactics", Science of Computer Programming, 14:305-321,
1990
- W. Turski and T. Maibaum, The Specification of
Computer Programs, Addison-Wesley, 1987.
- A. N. Whitehead and B. Russell, Principia
Mathematica, Cambridge University Press, 1910-1913.
09 Theory Development
- 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
-
Formal Methods.