Verified Computer Algebra in Acl2

Inmaculada Medina‐Bulo,Francisco Palomo-Lozano,José A. Alonso-Jiménez,José–Luis Ruiz–Reina

Artificial Intelligence and Symbolic Computation（2004）

引用 7|浏览5

暂无评分

摘要

In this paper, we present the formal verification of a Common Lisp implementation of Buchberger’s algorithm for computing Gröbner 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.

查看译文

关键词

Decision Procedure, Computer Algebra, Computer Algebra System, Polynomial Ideal, Proof Step

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要