Contexts in Mathematical Reasoning and Computation
William M. Farmer, Joshua D. Guttman, F. Javier Thayer
1995
Abstract
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.