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 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.
To prove the proposition we have to find an inhabitant of the type (Refl).
But in computer algebra I would have thought this equation would be an
element of some Equation type (I'm skipping over a lot of details).
Do you think both of these approaches could be brought together in a
consistent and elegant way?
Also my (limited) understanding is that Coq prevents inconsistencies
which makes it not Turing complete and therefore cant do everything
Axiom can do?
Martin
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-developer
