axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] QED Manifesto and Symbolic Algebra


From: Tim Daly
Subject: [Axiom-developer] QED Manifesto and Symbolic Algebra
Date: Sat, 22 Dec 2018 17:17:51 -0500

9. Too little care for rigor. It is notoriously easy to find "bugs" in
algorithms for symbolic
computation. To make matters worse, these errors are often regarded as
of no significance
by their authors, who plead that the result returned is true "except
on a set of measure
zero", without explicitly naming the set involved. The careful
determination, nay, even
proof, of precisely which conditions under which a result is true is
essential for building
the structure of mathematics so that one can depend on it. The QED
system will support
the development of symbolic algebra programs in which formal proofs of
correctness of
derivations are provided, along with the precise statement of
conditions under which the
results are true.



reply via email to

[Prev in Thread] Current Thread [Next in Thread]