[Top][All Lists]

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

Re: [Axiom-developer] Why proving Axiom correct is important

From: Martin Baker
Subject: Re: [Axiom-developer] Why proving Axiom correct is important
Date: Fri, 08 May 2015 16:20:45 +0100
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

On 08/05/15 10:02, address@hidden 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.


I am currently reading Nipkow/Klien [1] just to get a top level view of the subject (I have not looked at any research papers).

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.

I get the impression that what proof assistants / interactive theorem provers are about is proving equations/theories from other theories using logic and proof methods like induction. I think what you are talking about is proving algorithms correct (Semantics?) this is covered in part 2 of the book. Do you think these sort of approaches: Denotational Semantics, Small-step Semantics, Big-step Semantics and so on are what you are aiming at?

I get the impression that using a separate proof assistant is not ideal and there would be a lot of advantages in combining the symbolic algebra program (Axiom) with the logic/proof assistant. Apart from anything else the learning curve is as steep as Axiom! The problem for me is the massive and confusing overlap of these types of program. Not just the program but, more importantly, the libraries. As you can see from the libraries here:
it contains most of the same algebras as Axiom but in a slightly different hierarchy.

A possible first step would be to encode axioms/rules/identities in each Axiom category/domain. If nothing else this would allow automatic generation of test code at random values, this is not proof but it would be a first step to proofs at a later stage.


[1] Concrete Semantics with Isabelle/HOL, Nipkow/Klien, 2014, ISBN 978-3-319-10541-3

reply via email to

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