Martin,
>If you are using COQ then why not just map the COQ library entries into
>the Axiom categories?
>So if we take part of the base library here:
>https://coq.inria.fr/library/Coq.Arith.Mult.html#
>So the appropriate Axiom category could have an entry like:
>Zero property
>Lemma mult_0_r :
I had actually had something similar in one of OpenAxiom's branch.
On Sat, May 9, 2015 at 3:37 AM, Martin Baker wrote:
> On 08/05/15 21:40, d...@axiom-developer.org wrote:
>
>> There exists a few mathematical axiom statements in the category book
>> (Volume 10.2), associated with each category
On 08/05/15 21:40, d...@axiom-developer.org wrote:
There exists a few mathematical axiom statements in the category book
(Volume 10.2), associated with each category (look at SemiGroup for
example). The intention is to decorate all of the categories and
domains with mathematical axioms which can
Martin,
>The book is based around Isabelle/HOL so if you don't want to use
>Isabelle the book may not be of interest to you? I have only just
>started reading the book so I don't have any great insights to give.
Actually, Lamport's "How to write 21st Century Proofs" and
"Specifying Systems" is
On 08/05/15 10:02, d...@axiom-developer.org wrote:
Axiom Volume 13 is the start of the pile. If you find any papers
or articles that might be of interest to the goal, please let me know.
Tim,
I am currently reading Nipkow/Klien [1] just to get a top level view of
the subject (I have not looke
Mathematicans need to be able to rely on the algorithms.
http://nautil.us/issue/24/error/in-mathematics-mistakes-arent-what-they-used-to-be
___
Axiom-developer mailing list
Axiom-developer@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-devel
