4 ms·
Solving Rings in Agda
- krapht 8y agoWhenever 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.
- jedharris 8y agoI'm happy this exists, and that Agda has the facilities to make it feasible, but sad that automated formal systems are so primitive compared to software development tools. Is this gap just lack of motivation for more people to contribute, or the culture of formal systems, or some source of technical barriers, or ??
- riku_iki 8y agoHow one can type that ℕ and ℤ on the regular keyboard?..
- m_j_g 8y agoin atom plugin for agda you just typing \bn or \bz , full reference here: https://people.inf.elte.hu/divip/AgdaTutorial/Symbols.html#blackboard-bold-letters https://people.inf.elte.hu/divip/AgdaTutorial/Symbols.html#b...
- deleted 8y ago[deleted]
- michaelsbradley 8y agofor Emacs users see: https://agda.readthedocs.io/en/latest/tools/emacs-mode.html https://agda.readthedocs.io/en/latest/tools/emacs-mode.html