Hello, Sorry for the delay.
On Sat, Apr 7, 2012 at 11:23 PM, Ronan Lamy <[email protected]> wrote: > Le samedi 07 avril 2012 à 21:55 +0300, Sergiu Ivanov a écrit : >> >> 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. Thank you, Ronan! I have more or less read both articles and it looks like they aren't going to be of much help either for the project I have drafted for this summer or for the eventual implementation of diagram chasing. The reason is as follows: both articles focus on proof checkers like Isabelle [0] or Nuprl [1]. The authors construct a formal framework for categories and then formulate concrete situations and ask concrete questions. While this is all very nice and cool, it has two major disadvantages: * the actual reasoning work is done by the corresponding proof checker, and it is too general to directly adapt the ideas in it and use them in SymPy; * neither of the papers actually speaks of diagram chasing in a general setup. I'm not yet sure as to how much _exactly_ information useful for the category theory module can be extracted from these articles, but it looks like they are not that useful, after all :-( Sergiu [0] http://www.cl.cam.ac.uk/research/hvg/isabelle/ [1] http://www.nuprl.org/ -- 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.
