Advertisement

Reasoning with contexts

  • William M. Farmer
  • Joshua D. Guttman
  • F. Javier Thayer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 722)

Abstract

Contexts are sets of formulas used to manage the assumptions that arise in the course of a mathematical deduction or calculation. This paper describes some techniques for symbolic computation that are dependent on using contexts, and are implemented in IMPS, an Interactive Mathematical Proof System.

Keywords

Algebraic Manipulation Symbolic Computation Critical Pair Automate Deduction Theorem Application 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    R. S. Boyer and J. Strother Moore. Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. Technical Report ICSCA-CMP-44, Institute for Computing Science, University of Texas at Austin, January 1985.Google Scholar
  2. 2.
    D. Craigen, S. Kromodimoeljo, I. Meisels, B. Pase, and M. Saaltink. Eves system description. In D. Kapur, editor, Automated Deduction—CADE-11, volume 607 of Lecture Notes in Computer Science, pages 771–775. Springer-Verlag, 1992.Google Scholar
  3. 3.
    W. M. Farmer. A simple type theory with partial functions and subtypes. Annals of Pure and Applied Logic. Forthcoming.Google Scholar
  4. 4.
    W. M. Farmer. A partial functions version of Church's simple theory of types. Journal of Symbolic Logic, 55:1269–91, 1990.Google Scholar
  5. 5.
    W. M. Farmer, J. D. Guttman, and F. J. Thayer. IMPS: an Interactive Mathematical Proof System. Journal of Automated Reasoning. Forthcoming.Google Scholar
  6. 6.
    W. M. Farmer, J. D. Guttman, and F. J. Thayer. IMPS: System description. In D. Kapur, editor, Automated Deduction—CADE-11, volume 607 of Lecture Notes in Computer Science, pages 701–705. Springer-Verlag, 1992.Google Scholar
  7. 7.
    W. M. Farmer, J. D. Guttman, and F. J. Thayer. Little theories. In D. Kapur, editor, Automated Deduction—CADE-11, volume 607 of Lecture Notes in Computer Science, pages 567–581. Springer-Verlag, 1992.Google Scholar
  8. 8.
    J. D. Guttman. A proposed interface logic for verification environments. Technical Report M91-19, The MITRE Corporation, 1991.Google Scholar
  9. 9.
    M. Kohlhase. Unification in order-sorted type theory. In A. Voronkov, editor, Logic Programming and Automated Reasoning, volume 624 of Lecture Notes in Computer Science, pages 421–432. Springer-Verlag, July 1992.Google Scholar
  10. 10.
    L. G. Monk. Inference rules using local contexts. Journal of Automated Reasoning, 4:445–462, 1988.CrossRefGoogle Scholar
  11. 11.
    S. Owre, J. M. Rushby, and N. Shankar. pvs: A prototype verification system. In D. Kapur, editor, Automated Deduction—CADE-11, volume 607 of Lecture Notes in Computer Science, pages 748–752. Springer-Verlag, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • William M. Farmer
    • 1
  • Joshua D. Guttman
    • 1
  • F. Javier Thayer
    • 1
  1. 1.The MITRE CorporationBedfordUSA

Personalised recommendations