| Autor: |
José A. Alonso-Jiménez, José-Luis Ruiz-Reina, Inmaculada Medina-Bulo, Francisco Palomo-Lozano |
| Rok vydání: |
2004 |
| Předmět: |
|
| Zdroj: |
Artificial Intelligence and Symbolic Computation ISBN: 9783540232124 |
| DOI: |
10.1007/978-3-540-30210-0_15 |
| Popis: |
In this paper, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Grobner bases of polynomial ideals. This work is carried out in the Acl2 system and shows how verified Computer Algebra can be achieved in an executable logic. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
