[Top][All Lists]

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

Re: [Axiom-developer] Axiom's Sane redesign musings

From: Martin Baker
Subject: Re: [Axiom-developer] Axiom's Sane redesign musings
Date: Wed, 19 Jun 2019 16:29:31 +0100
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.7.0

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.


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?


reply via email to

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