IMPS: An Interactive Mathematical Proof System

Copyright (c) 1990-2001 The MITRE Corporation

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

Full IMPS Bibliography

  1. Abstract data types in many-sorted second-order logic
    W. M. Farmer
    Technical Report M87-64, 29 pp., The MITRE Corporation, October 1987.
  2. A partial functions version of Church's simple theory of types
    W. M. Farmer
    Journal of Symbolic Logic, 55:1269-1291, 1990.
  3. A simple type theory with partial functions and subtypes
    W. M. Farmer
    Annals of Pure and Applied Logic, 64:211-240, 1993.
  4. A general method for safely overwriting theories in mechanized mathematics systems PostScript PDF
    W. M. Farmer
    Technical Report, 21 pp., The MITRE Corporation, 1994.
  5. 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.
  6. Reasoning about partial functions with the aid of a computer
    W. M. Farmer
    Erkenntnis, 43:279-294, 1995.
  7. 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.
  8. 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.
  9. STMM and partial functions
    W. M. Farmer
    In: M. Kerber, ed., Proceedings of the Workshop on the Mechanization of Partial Functions, pp. 3-14, CADE-15, Lindau, Germany, July 5, 1998.
    Preliminary version of STMM: a Set Theory for Mechanized Mathematics.
  10. 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.
  11. An infrastructure for intertheory reasoning PostScript PDF
    W. M. Farmer
    In: D. McAllester, ed., Automated Deduction--CADE-17, LNCS, 1831:115-131, 2000.
  12. 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.
  13. STMM: a Set Theory for Mechanized Mathematics PostScript PDF
    W. M. Farmer
    Journal of Automated Reasoning, 26:269-289, 2001.
  14. 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.
  15. 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.
  16. 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.
  17. IMPS: an Interactive Mathematical Proof System (system description)
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    In: M. E. Stickel, ed., 10th International Conference on Automated Deduction, LNCS, 449:653-654, 1990.
    Abstract.
  18. IMPS: system description PostScript PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    In: D. Kapur, ed., Automated Deduction--CADE-11, LNCS, 607: 701-705, 1992.
  19. 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.
  20. 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.
  21. 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.
  22. Reasoning with contexts
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    In: A. Miola, ed., Design and Implementation of Symbolic Computation Systems, LNCS, 722:216-228, 1993.
    Preliminary version of Contexts in mathematical reasoning and computation.
  23. Contexts in mathematical reasoning and computation
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    Journal of Symbolic Computation, 19:201-216, 1995.
  24. 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.
  25. Formal numerical program analysis PostScript PDF
    W. M. Farmer and F. J. Thayer
    Technical Report, 52 pp., The MITRE Corporation, 1994.
  26. 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.
  27. A Proposed interface logic for verification environments
    J. D. Guttman
    Technical Report M91-19, The MITRE Corporation, 1991.
  28. Building verification environments from components: a position paper
    J. D. Guttman
    In: Proceedings, Workshop on Effective Use of Automated Reasoning Technology in System Development, pp. 4-17, Naval Research Laboratory, Washington, D.C., April 1992.
  29. A simple virtual memory scheme formalized in IMPS PostScript PDF
    J. D. Guttman
    Technical Report, The MITRE Corporation, 1994.
  30. Three applications of formal methods at MITRE
    J. D. Guttman and D. M. Johnson
    In: M. Naftalin, T. Denvir, and M. Bertran, eds., FME '94: Industrial Benefits of Formal Methods, LNCS, 873:55-65, 1994.
  31. PDLM: a Proof Development Language for Mathematics
    L. G. Monk
    Technical Report M86-37, The MITRE Corporation, 1986.
  32. Inference rules using local contexts
    L. G. Monk
    Journal of Automated Reasoning, 4:445-462, 1988.
  33. The T Manual, Fifth Edition PostScript PDF
    J. A. Rees, N. I. Adams, and J. R. Meehan
    Computer Science Department, Yale University, 1990.
  34. Obligated term replacements
    F. J. Thayer
    Technical Report MTR-10301, The MITRE Corporation, 1987.
  35. An approach to process algebra using IMPS PostScript PDF
    F. J. Thayer
    Technical Report MP-94B193, The MITRE Corporation, 1994.
  36. Copy on write PostScript PDF
    F. J. Thayer and J. D. Guttman
    Technical Report, The MITRE Corporation, 1995.