Le samedi 07 avril 2012 à 21:55 +0300, Sergiu Ivanov a écrit : > On Sat, Apr 7, 2012 at 9:12 PM, Tom Bachmann <[email protected]> wrote: > >>> Hm. It seems my perspective on category theory is indeed skewed towards > >>> applications. I have seen some horrendous diagrams, but only in settings > >>> where the desired method of proof is diagram chasing. > >> > >> > >> I see. > >> > >> Diagram chasing is a very cool thing, I would be very glad to give it > >> a try at implementing. > >> > >> Is it OK if I add this point to my proposal on the wiki and post a > >> corresponding comment on Melange? :-) > >> > > > > Sure, go ahead! > > I am pleasantly surprise to announce that I have actually found a > paper which seems to be about (semi-)automatic diagram chasing! > > A mechanically assisted constructive proof in category theory > James A. Altucher and Prakash Panangaden > > http://www.springerlink.com/content/f118u0u0338470u5/ > > The abstract looks promising.
It's from 1990 though, and doesn't seem to have had a lot of follow-up. http://users.cecs.anu.edu.au/~okeefe/work/fcat4cats04.pdf might be more current. > > Unfortunately, I don't have an ACM or Sprigner subscription, and I'm > not sure my institution has it. I don't seem to be able to find a > free download link either. > > Sergiu > -- You received this message because you are subscribed to the Google Groups "sympy" group. To post to this group, send email to [email protected]. To unsubscribe from this group, send email to [email protected]. For more options, visit this group at http://groups.google.com/group/sympy?hl=en.
