IMPS: An Interactive Mathematical Proof System

Copyright (c) 1990-2001 The MITRE Corporation

Authors: W. M. Farmer, J. D. Guttman, F. J. Thayer

Major IMPS Papers

  1. A partial functions version of Church's simple theory of types
    W. M. Farmer
    Journal of Symbolic Logic, 55:1269-1291, 1990.
  2. A simple type theory with partial functions and subtypes
    W. M. Farmer
    Annals of Pure and Applied Logic, 64:211-240, 1993.
  3. A general method for safely overwriting theories in mechanized mathematics systems PostScript PDF
    W. M. Farmer
    Technical Report, 21 pp., The MITRE Corporation, 1994.
  4. Theory interpretation in simple type theory PostScript PDF
    W. M. Farmer
    In: J. Heering et al., eds., Higher-Order Algebra, Logic, and Term Rewriting, LNCS, 816:96-123, 1994.
  5. Reasoning about partial functions with the aid of a computer
    W. M. Farmer
    Erkenntnis, 43:279-294, 1995.
  6. Mechanizing the traditional approach to partial functions PostScript PDF
    W. M. Farmer
    In: W. Farmer, M. Kerber, and M. Kohlhase, eds., Proceedings of the Workshop on the Mechanization of Partial Functions, pp. 27 -32, CADE-13, Rutgers University, New Brunswick, New Jersey, July 30, 1996.
    Abbreviated version of Reasoning about partial functions with the aid of a computer.
  7. The Interactive Mathematics Laboratory online
    W. M. Farmer
    In: Proceedings of the 31st Annual Midwest Instruction and Computing Symposium (MICS '98), pp. 84-94, Fargo, North Dakota and Moorhead, Minnesota, April 16-18, 1998.
  8. A scheme for defining partial higher-order functions by recursion PostScript PDF online
    W. M. Farmer
    In: A. Butterfield, ed., 3rd Irish Workshop on Formal Methods, 13 pp., electronic Workshops in Computing, Springer-Verlag, 1999.
  9. An infrastructure for intertheory reasoning PostScript PDF
    W. M. Farmer
    In: D. McAllester, ed., Automated Deduction--CADE-17, LNCS, 1831:115-131, 2000.
  10. A proposal for the development of an interactive mathematics laboratory for mathematics education PostScript PDF
    W. M. Farmer
    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.
  11. STMM: a Set Theory for Mechanized Mathematics PostScript PDF
    W. M. Farmer
    Journal of Automated Reasoning, 26:269-289, 2001.
  12. A set theory with support for partial functions PostScript PDF
    W. M. Farmer and J. D. Guttman
    In: Partiality and Modality, eds., E. Thijsse, F. Lepage, and H. Wansing, special issue of Studia Logica, 66:59-78, 2000.
  13. IMPS: an updated system description PostScript PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer Fábrega
    In: M. McRobbie and J. Slaney, eds., Automated Deduction--CADE-13, LNCS, 1104:298-302, 1996.
  14. Proof script pragmatics in IMPS PostScript PDF
    W. M. Farmer, J. D. Guttman, M. E. Nadel, and F. J. Thayer
    In: A. Bundy, ed., Automated Deduction--CADE-12, LNCS, 814: 356-370, 1994.
  15. Little theories PostScript PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    In: D. Kapur, ed., Automated Deduction--CADE-11, LNCS, 607:567-581, 1992.
  16. IMPS: an Interactive Mathematical Proof System PostScript PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    Journal of Automated Reasoning, 11:213-248, 1993.
  17. The IMPS user's manual HTML PostScript PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    Technical Report M-93B138, 289 pp., The MITRE Corporation, November 1993.
  18. Contexts in mathematical reasoning and computation
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    Journal of Symbolic Computation, 19:201-216, 1995.
  19. Two computer-supported proofs in metric space topology PostScript PDF
    W. M. Farmer and F. J. Thayer
    Notices of the American Mathematical Society, 38:1133-1138, 1991.
  20. Formal numerical program analysis PostScript PDF
    W. M. Farmer and F. J. Thayer
    Technical Report, 52 pp., The MITRE Corporation, 1994.
  21. Transformers for symbolic computation and formal deduction PostScript PDF
    W. M. Farmer and M. v. Mohrenschildt
    In: S. Colton, U. Martin and V. Sorge, eds., Proceedings of the Workshop on the Role of Automated Deduction in Mathematics, pp. 36-45, CADE-17, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 20-21, 2000.
  22. A simple virtual memory scheme formalized in IMPS PostScript PDF
    J. D. Guttman
    Technical Report, The MITRE Corporation, 1994.
  23. An approach to process algebra using IMPS PostScript PDF
    F. J. Thayer
    Technical Report MP-94B193, The MITRE Corporation, 1994.
  24. Copy on write PostScript PDF
    F. J. Thayer and J. D. Guttman
    Technical Report, The MITRE Corporation, 1995.