Implementation in Acl2 of Well-Founded Polynomial Orderings
Inmaculada Medina‐Bulo, Francisco Palomo‐Lozano, José A. Alonso-Jiménez · 2002
This paper presents how the development of a polynomial ordering andthe verio/cation of its properties can be o/t in the framework of Acl2. The key result is the well-foundedness of a polynomial ordering, whichis proved by a proper ordinal embedding. Normalized polynomials have been formalized to achieve this. The motivation for this workis to serve as a basis for proving the termination of certain reduction relations on polynomials in Acl2.