[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: David MENTRE
Subject: [Axiom-developer] [Inmaculada Medina Bulo] Polynomials in ACL2
Date: Mon, 09 Feb 2004 22:19:19 +0100
User-agent: Gnus/5.1006 (Gnus v5.10.6) Emacs/21.3 (gnu/linux)


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.


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

reply via email to

[Prev in Thread] Current Thread [Next in Thread]