Contexts in Mathematical Reasoning and Computation

Contexts are sets of formulas used to manage the assumptions that arise in the course of a mathematical deduction or calculation. Although context-dependent reasoning is commonplace in informal mathematics, most contemporary symbolic computation systems do not utilize contexts in sophisticated ways. This paper describes some context-based techniques for symbolic computation, including techniques for reasoning about definedness, simplifying abstract algebraic expressions, and computing with theorems. All of these techniques are implemented in the IMPS Interactive Mathematical Proof System. The paper also proposes a general mathematics laboratory that combines the functionality of current symbolic computation systems with the facilities of a theorem proving system like IMPS.