{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T04:40:43Z","timestamp":1775018443656,"version":"3.50.1"},"reference-count":16,"publisher":"Pleiades Publishing Ltd","issue":"4","license":[{"start":{"date-parts":[[2023,7,28]],"date-time":"2023-07-28T00:00:00Z","timestamp":1690502400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,7,28]],"date-time":"2023-07-28T00:00:00Z","timestamp":1690502400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Program Comput Soft"],"published-print":{"date-parts":[[2023,8]]},"DOI":"10.1134\/s0361768823040102","type":"journal-article","created":{"date-parts":[[2023,7,28]],"date-time":"2023-07-28T09:02:21Z","timestamp":1690534941000},"page":"199-214","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Admissible Ordering on Monomials is Well-Founded: A Constructive Proof"],"prefix":"10.1134","volume":"49","author":[{"given":"S. D.","family":"Meshveliani","sequence":"first","affiliation":[]}],"member":"137","published-online":{"date-parts":[[2023,7,28]]},"reference":[{"key":"3737_CR1","unstructured":"Meshveliani, S.D., On dependent types and intuitionism in programming mathematics, 2017. https:\/\/arxiv.org\/find\/all\/1\/all:+Mechveliani\/0\/1\/0\/all\/0\/1."},{"key":"3737_CR2","unstructured":"Meshveliani, S.D., AdmissiblePPO-wellFounded \u2013 A program in the Agda language for a constructive proof of Dickson\u2019s lemma and for a theorem of wellfoundedness of any admissible ordering on monomials of polynomials, 2022. www.botik.ru\/pub\/local\/Mechveliani\/inAgda\/admissiblePPO-wellFounded.zip."},{"key":"3737_CR3","volume-title":"A formal proof of Dickson\u2019s lemma in ACL2, Logic Program., Artif. Intell., Reasoning","author":"F.J. Martin-Mateos","year":"2003","unstructured":"Martin-Mateos, F.J., Alonso, J.A., Hidalgo, M.J., and Ruiz-Reina, J.L., A formal proof of Dickson\u2019s lemma in ACL2, Logic Program., Artif. Intell., Reasoning, Vardi, M.Y. and Voronkov, A., Eds., 2003, pp. 49\u201358."},{"key":"3737_CR4","unstructured":"Agda Wiki, A proof assistant, A dependently typed functional programming language and its system. http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php."},{"key":"3737_CR5","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-04652-0_5","volume":"5832","author":"U. Norell","year":"2008","unstructured":"Norell, U., Dependently typed programming in Agda, Adv. Funct. Program., 2008, vol. 5832, pp. 230\u2013266.","journal-title":"Adv. Funct. Program."},{"key":"3737_CR6","volume-title":"Gr\u00f6bner Bases: An Algorithmic Method in Polynomial Ideal Theory","author":"B. Buchberger","year":"1983","unstructured":"Buchberger, B., Gr\u00f6bner Bases: An Algorithmic Method in Polynomial Ideal Theory, CAMP, 1983."},{"key":"3737_CR7","doi-asserted-by":"crossref","unstructured":"Coquand, Th. and Persson, H., Gr\u00f6bner bases in type theory, 1998. https:\/\/www.researchgate.net\/publication\/221186683_Grobner_Bases_in_Type_Theory.","DOI":"10.1007\/3-540-48167-2_3"},{"key":"3737_CR8","doi-asserted-by":"crossref","unstructured":"Th\u00e9ry, L., A machine-checked implementation of Buchberger\u2019s algorithm, J. Autom. Reasoning, 2001, pp.\u00a0107\u2013137.","DOI":"10.1023\/A:1026518331905"},{"key":"3737_CR9","unstructured":"Romanenko, S.A., Proof of Higman\u2019s lemma (for two letters) formalized in Agda, 2017. \nhttps:\/\/pat.keldysh.ru\/~roman\/doc\/talks\/2017_Romanenko__Higman's_lemma_for_2_letters_in_Agda_ru__slides.pdf. Agda program for the proof (in the Berghofer folder): https:\/\/github.com\/sergei-romanenko\/agda-Higman-lemma."},{"key":"3737_CR10","doi-asserted-by":"crossref","unstructured":"Robbiano, L., Term orderings on the polynomial ring, Proc. Eur. Conf. Comput. Algebra (EUROCAL), Linz, 1986, pp. 513\u2013517.","DOI":"10.1007\/3-540-15984-3_321"},{"key":"3737_CR11","volume-title":"Combinatory Logic","author":"H.B. Curry","year":"1958","unstructured":"Curry, H.B. and Feys, R., Combinatory Logic, 1958, vol. 1."},{"key":"3737_CR12","volume-title":"The formulae-as-types notion of construction, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"W.A. Howard","year":"1980","unstructured":"Howard, W.A., The formulae-as-types notion of construction, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Boston: Academic Press, 1980, pp. 479\u2013490."},{"key":"3737_CR13","series-title":"On constructive mathematics, Problems of constructive direction in mathematics, Part 2: Constructive mathematical analysis, Tr. Mat. Inst.","volume-title":"V.A. Steklova (Proc. Steklov Inst. Math.)","author":"A.A. Markov","year":"1962","unstructured":"Markov, A.A., On constructive mathematics, Problems of constructive direction in mathematics, Part 2: Constructive mathematical analysis, Tr. Mat. Inst. \n               im. \n               V.A. Steklova (Proc. Steklov Inst. Math.), Izd. Akad. Nauk SSSR, Moscow, 1962, pp. 8\u201314."},{"key":"3737_CR14","volume-title":"Intuitionistic Type Theory","author":"Per Martin-L\u00f6f","year":"1984","unstructured":"Per Martin-L\u00f6f, Intuitionistic Type Theory, Bibliopolis, 1984."},{"key":"3737_CR15","unstructured":"Stricland, N.P., Euclid\u2019s theorem: An annotated proof in Agda that there are infinitely many primes. https:\/\/nextjournal.com\/agda\/euclid-theorem."},{"key":"3737_CR16","doi-asserted-by":"crossref","unstructured":"Vytiniotis, D., Coquand, Th., and Wahlstedt, D., Stop when you are almost-full: Adventures in constructive termination, Proc. Conf. Interactive Theorem Proving (ITP), 2012, pp. 250\u2013265.","DOI":"10.1007\/978-3-642-32347-8_17"}],"container-title":["Programming and Computer Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768823040102.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1134\/S0361768823040102","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768823040102.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T02:52:32Z","timestamp":1775011952000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1134\/S0361768823040102"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,28]]},"references-count":16,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,8]]}},"alternative-id":["3737"],"URL":"https:\/\/doi.org\/10.1134\/s0361768823040102","relation":{},"ISSN":["0361-7688","1608-3261"],"issn-type":[{"value":"0361-7688","type":"print"},{"value":"1608-3261","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,7,28]]},"assertion":[{"value":"23 September 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 November 2022","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 November 2022","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 July 2023","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The author declares that he has no conflicts of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"CONFLICT OF INTEREST"}}]}}