[Agda] Ramsey theorem

[Josef Svenningsson]

If you're interested in Ramsey's theorem for the purpose of termination I
suggest you read the paper "Stop When You Are Almost-Full", by Dimitrios
Vytiniotis, Thierry Coquand and David Wahlstedt. They develop an
intuitionistic Ramsey theorem to be used for proving termination. The paper
uses Coq but there is an Agda formalization here:
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.IntuitionisticRamseyTheorem

Josef



On Fri, Jul 4, 2014 at 1:29 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:

> People,
>
> is there publicly available a proof  in Agda  of the  Ramsey's theorem
> (about the size of a monochromatic sub-graph in a complete graph)
> ?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> 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/20140704/4f7a53a0/attachment.html