Admissible ordering on monomials is well-founded: a constructive proof

DOI10.1134/S0361768823040102MaRDI QIDQ6094419zbMATH OpenFDO

Authors S. D. Meshveliani

Publication date 13 September 2023

Published in Programming and Computer Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1134/S0361768823040102

zbMATH Keywords

admissible orderingcomputer algebraconstructive proofDickson's lemmapolynomials

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Other constructive mathematics (03F65) Formalization of mathematics in connection with theorem provers (68V20) Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 1420784
• An effective proof of the well-foundedness of the multiset path ordering
• scientific article; zbMATH DE number 2185669
• scientific article; zbMATH DE number 1318515
• Standard bases for general coefficient rings and a new constructive proof of Hilbert's basis theorem

Cites work

• A formal proof of Dickson's lemma in ACL2
• A machine-checked implementation of Buchberger's algorithm
• Combinatory logic. With two sections by William Craig.
• Dependently typed programming in Agda
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 3935185 (Why is no real title available?)
• scientific article; zbMATH DE number 3941661 (Why is no real title available?)
• scientific article; zbMATH DE number 1420784 (Why is no real title available?)
• Stop when you are almost-full. Adventures in constructive termination

This page was built for publication: Admissible ordering on monomials is well-founded: a constructive proof

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6094419)