Electronic communication of Mathematics and the Interaction of computer Algebra Systems and Proof Assistants

摘要

Present day computer algebra systems (CASs) and proof assistants (Pas) are specialized programs that help humans with mathematical computations and deductions. Although several such systems are impressive, they all have certain limitations. In most CASs side conditions that are essential for the truth of an equality are not formulated moreover there are bugs. The Pas have a limited power for computing and hence also for assistance with proofs.