4 ms·
Whenever I read a technical overview like this, I like to see references to existing literature. This report doesn't do this, see for example https://link.sprin
by krapht 8y ago
Whenever I read a technical overview like this, I like to see references to existing literature. This report doesn't do this, see for example https://link.springer.com/chapter/10.1007/11541868_7 https://link.springer.com/chapter/10.1007/11541868_7 which is basically the same thing but in Coq.
- oisdk 8y agoAuthor here! It's my fault the code and report are a little disorganized, but there is a related work section in the full report (https://github.com/oisdk/agda-ring-solver-report/blob/master/report.pdf https://github.com/oisdk/agda-ring-solver-report/blob/master...) which mentions that paper. Also, if you click through to the section on the algorithm itself (https://oisdk.github.io/agda-ring-solver/Polynomial.NormalForm.html https://oisdk.github.io/agda-ring-solver/Polynomial.NormalFo...) you'll see a link to the same paper.