Artigo Revisado por pares

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

2008; Taylor & Francis; Volume: 87; Issue: 1 Linguagem: Inglês

10.1080/00207160701864459

ISSN

1029-0265

Autores

Adam Naumowicz,

Tópico(s)

Formal Methods in Verification

Resumo

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 algebraMIZAR Gröbner bases 2000 AMS Subject Classification : 03B3568T15 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.

Referência(s)