![[malb]](http://www.informatik.uni-bremen.de/~malb/images/blog.png "back to main"){kind=small}
PhD Thesis on F5
May I point my dear reader’s attention to Justin Gash’s PhD thesis on F5. It is mainly referred to because it points out an error in the proof of termination in the original F5 paper. I started reading the thesis today (in preparation of SD12 in San Diego) and it already helped me a lot to understand the algorithm. As a consequence I added a bunch of comments from Justin’s thesis to my toy F5 implementation which should explain a bit what is going on.
However, since Justin’s pseudocode is not identical with John Perry’s pseudocode (on which my implementation is based) things don’t match up perfectly. For instance, I still need to figure out what the differences in critical_pair exactly come down to.
