On 08/05/15 10:02, [email protected] 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 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:
http://isabelle.in.tum.de/dist/library/HOL/index.html
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.
Martin
[1] Concrete Semantics with Isabelle/HOL, Nipkow/Klien, 2014, ISBN
978-3-319-10541-3
_______________________________________________
Axiom-developer mailing list
[email protected]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
