Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier Contexts in mathematical reasoning and computation. (English) Zbl 0836.68107 J. Symb. Comput. 19, No. 1-3, 201-216 (1995). Summary: 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. Cited in 1 Document MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68W30 Symbolic computation and algebraic computation 03B35 Mechanization of proofs and logical operations Keywords:contexts; symbolic computation; reasoning; Interactive Mathematical Proof System Software:PVS PDFBibTeX XMLCite \textit{W. M. Farmer} et al., J. Symb. Comput. 19, No. 1--3, 201--216 (1995; Zbl 0836.68107) Full Text: DOI