01-08-2023
Admissible Ordering on Monomials is Well-Founded: A Constructive Proof
Published in: Programming and Computer Software | Issue 4/2023
Log inActivate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Abstract
Coq
and Agda
), a somewhat stronger condition (in constructive mathematics) of the well-foundedness of the ordering (in its constructive version) is required. We propose a constructive proof of this theorem (T) for <\(_{e}\), which is based on a known method that we refer to here as the “pattern method.” This theorem on the well-foundedness of an arbitrary admissible ordering is also important in itself, independently of the NF algorithm. We are not aware of any other works on constructive proof of this theorem. However, it turns out that it follows, not very difficultly, from the results achieved by other researchers in 2003. We program this proof in the Agda
language in the form of our library AdmissiblePPO-wellFounded
of provable computational algebra programs. This development also uses the theorem to prove termination of the NF algorithm for polynomials. Thus, the library also contains a set of provable programs for polynomial algebra, which is significantly larger than that needed to prove Theorem T.