--- Begin Message ---
Subject: |
Polynomials in ACL2 |
Date: |
Mon, 9 Feb 2004 13:26:50 +0100 |
User-agent: |
KMail/1.5.4 |
El Viernes, 6 de Febrero de 2004 23:43, Julien Schmaltz escribió:
> Hi,
>
> I need to perform basic operations on polynomials: addition, substraction,
> multiplication and division of two polynomials P(x) and M(x).
> Have someone already worked with these objects? In that case, is there a
> book I can use?
Hi Julien,
Sorry for the delay in replying.
I have implemented and certified a book about polynomials. In this book, you
can find addition and multiplication of two polynomials, and negation of a
polynomial. The fundamental properties have been verified with ACL2. However,
it does not include division of polynomials.
I presented a paper about this, "Automatic Verification of Polynomial Rings
Fundamental Properties in ACL2", in ACL2 Workshop 2000.
This paper presents a formalization of multivariate polynomials over a
coefficient field (initially, Q) along with the verification of its ring
properties. Later, I formalized multivariate polynomials over an arbitrary
(abstract) ring.
However, an inconvenient is that this particular formalization is not
efficient. In fact, I have the intention of improving it.
Regards, Inma
--
Inmaculada Medina Bulo
Departamento de Lenguajes y Sistemas Informáticos
Escuela Superior de Ingeniería
C/ Chile s/n. 11008 Cádiz
Tfno: 956 015730 FAX: 956015139
--- End Message ---