Reasoning with contexts

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.