MathScheme
An Integrated Framework For Computer Algebra
And Computer Theorem Proving
MathScheme is a project to develop a new approach to mechanized
mathematics in which computer algebra and computer theorem proving are
merged without sacrificing power or soundness. The first goal of the
project is to develop a formal framework that integrates and
generalizes symbolic computation and formal deduction. The second
project goal is to design and implement a mechanized mathematics
system based on the formal framework. The long-range goal is to
build, on top of the mechanized mathematics system, an interactive
mathematics laboratory that provides an integrated set of tools
for facilitating and managing mathematical reasoning.