[Agda] proof by AC-reduction
Nils Anders Danielsson
nad at chalmers.se
Wed Feb 20 17:48:58 CET 2013
On 2013-02-19 15:50, Serge D. Mechveliani wrote:
> Agda needs some proof assistants provided as additional libraries
> (some of them may be even in the Standard library).
Have you seen the ring solver that is part of the standard library?
http://www.cse.chalmers.se/~nad/listings/lib/README.Nat.html
http://www.cse.chalmers.se/~nad/listings/lib/README.Integer.html
This solver uses a technique called "proof by reflection", a technique
that can be used for other solvers as well. For instance, I have written
one for monoids:
http://www.cse.chalmers.se/edu/year/2012/course/afp/lectures/lecture11/html/Proof-by-reflection.html
I have also written one for equality proofs (intended to be used with
--without-K):
http://www.cse.chalmers.se/~nad/listings/equality/Equality.Tactic.html
--
/NAD
More information about the Agda
mailing list