Martin,
> Are there some fundamental compromises that have to be made when combining
> computer > algebra and proof technology?
> For instance in proof assistants, like Coq, equations are types for instance:
> x = x + 0
> is a proposition which, by Curry-Howard, can be represented as a type. T
On 19/06/2019 12:18, Tim Daly wrote:
The effort to
Prove Axiom Sane involves merging computer algebra and proof
technology so Axiom's algorithms have associated proofs.
Tim,
Are there some fundamental compromises that have to be made when
combining computer algebra and proof technology?
For
Sane: "rational, coherent, judicious, sound"
Axiom is computational mathematics, of course. The effort to
Prove Axiom Sane involves merging computer algebra and proof
technology so Axiom's algorithms have associated proofs.
The union of these two fields has made it obvious how far behind
Axiom ha
