Interfacing external CA systems for Gröbner bases computation in M izar proof checking
Adam Naumowicz · International Journal of Computer Mathematics · 2008
In this paper, we report on the results of a case study aimed at selecting a prospective CA system to be used by the Mizar proof-checking system for performing computations of Gröbner bases in Mizar’s module responsible for equality calculus. A rudimentary interface has been implemented for each of considered CA systems, and tested in order to assess its feasibility in connection with the Mizar proof checker.