[Axiom-developer] [Inmaculada Medina Bulo] Polynomials in ACL2

[David MENTRE]

Hello,

I've seen this email on ACL2 mailing list. Apparently, this person as
done some verification of (very simple) properties of polynomials. Might
be of some interest in the future if somebody wants to tackle Formal
Verification of Axiom.

Yours,
d.

> --- 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 ---