×

Contexts in mathematical reasoning and computation. (English) Zbl 0836.68107

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.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30 Symbolic computation and algebraic computation
03B35 Mechanization of proofs and logical operations

Software:

PVS
PDFBibTeX XMLCite
Full Text: DOI