Interfacing external CA systems for Gröbner bases computation in Mizar proof checking

Abstract

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.

Keywords:

• integrating automated deduction and computer algebra
• MIZAR
• Gröbner bases

2000 AMS Subject Classification :

• 03B35
• 68T15

Acknowledgements

I would like to thank very much all developers of various systems who responded to my query, many a time offering not just answers to my questions, but a lot of valuable information I could use in this case study: Sergey Lyalin (Arageli), Anna Bigatti (CoCoA), Dongming Wang (Epsilon), Stefan Kohl (GAP), Predrag Janicic (GCLC), Anders Jensen (Gfan), Markus Schmies (jtem), Michael Pohst (KANT/KASH), Dave Saunders (LinBox), Dan Grayson (Macaulay2), Karim Belabas (Pari-GP), Anne Fruehbis (Singular) and Bernard Mourrain (SYNAPS).

Notes

^†Available at http://cocoa.dima.unige.it/download/doc/help.pdf

^†See the article POLYEQ_3, the inference in line 873, MML Ver. 4.76.959.