[Agda] proof by AC-reduction

[Dan Rosén]

Incidentally, I wrote one for distributive lattices:

http://web.student.chalmers.se/~danr/DLSolver/DLSolver.Examples.html

It was inspired by NAD's monoid solver.

On Wed, Feb 20, 2013 at 5:48 PM, Nils Anders Danielsson <nad at chalmers.se>wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130220/ca14cbf7/attachment.html