{"entities":{"Q1899143":{"pageid":1909885,"ns":120,"title":"Item:Q1899143","lastrevid":43403719,"modified":"2025-07-25T12:30:23Z","type":"item","id":"Q1899143","labels":{"en":{"language":"en","value":"Proof-theoretic analysis of termination proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 802547"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1899143$DE959EB8-169C-4E15-8EDB-59AE516EBC2D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b9537f5a7f70ff03360c72092d2c1c24404e7186","datavalue":{"value":{"text":"Proof-theoretic analysis of termination proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1899143$F8E9ED88-5BA1-4206-B805-47CFD27D373E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3e5a0e421b01013fe1cfce39fb488b374319e1e8","datavalue":{"value":"0844.03031","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1899143$07FB6D77-DDAA-49DD-BB95-31930527F2D8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e927079e3a41124d6d882a1d4b49f326c731518d","datavalue":{"value":"10.1016/0168-0072(94)00056-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1899143$A42A0082-81BB-42FA-AB94-53BCFB8028C2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ca3d0fdc4dfe73f15e4cc6198de2fda062014c98","datavalue":{"value":{"entity-type":"item","numeric-id":204229,"id":"Q204229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1899143$5C4EB4BB-C4B6-44AC-90CB-F29CC4232C26","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1899143$F330468D-039C-4C83-BF8A-C958A19200CE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5bfc915913f56bda83b8f5a217ba51a7f0094c41","datavalue":{"value":{"time":"+1996-08-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1899143$751472A2-E6CA-49E2-8E74-76F49DD6BF13","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"679635a5fd6142e1dd9993ca8a30339b87699970","datavalue":{"value":"\\textit{E. A. Cicho\u0144} [in: Proof theory, Int. Summer School and Conf., Leeds, UK, 1990, 173-193 (1992; Zbl 0793.03057)] raised the question whether there is a relation between the order type of a termination ordering \\(\\prec\\) and the lengths of reduction sequences in a rewrite system reducing under \\(\\prec\\).   \\textit{D. Hofbauer} [Theor. Comput. Sci. 105, No. 1, 129-140 (1992; Zbl 0759.68045)] gave an answer to this question in case that \\(\\prec\\) is a multiset path ordering, \\textit{A. Weiermann} [ibid. 139, 355-362 (1995)] settled the problem for \\(\\prec\\) being a lexicographic path ordering. In both papers, the procedure is rather tedious. In the paper under review, the author gives an elegant solution for both kinds of termination orderings using proof-theoretical means.   He first proves the well-foundedness of the lexicographic path ordering \\(\\langle T, \\prec\\rangle\\) considering the accessible part \\(W\\) of \\(\\langle T, \\prec\\rangle\\) and showing that \\(W= T\\).   The crucial observation of the author is the following: For proving termination of a single finite rewrite system using lexicographical path ordering one does not need the full relation \\(\\prec\\) but only a suitable subset \\(\\prec_k\\) of it, for some \\(k\\in \\mathbb{N}\\) (Lemma 7). He defines for every \\(k\\) such a relation \\(\\prec_k \\subset \\prec\\) and proves that it is well-founded following the lines of the proof for \\(\\langle T, \\prec\\rangle\\). In this proof, the accessible part of \\(T\\) w.r.t. \\(\\prec_k\\) is already defined by a \\(\\Sigma_1^0\\)-formula. Thus the proof of well-foundedness of \\(\\prec_k\\) can be carried through in \\(\\Pi_2^0\\)-IA, i.e. \\(\\Pi_2^0\\)-IA \\(\\lvdash\\forall t\\) \\(t\\in W_k\\) holds, and therefore, by a result \\textit{Ch. Parsons} communicated in Notices AMS 13 (1966), there is some \\(\\alpha\\prec \\omega^\\omega\\) such that the length of every \\(\\prec_k\\)-decreasing sequence of elements of \\(W_k\\) starting with \\(t\\) is bounded by \\(F_\\alpha(t)\\), \\(F_\\alpha\\) being a function of the fast-growing hierarchy.   In the last section, the author indicates how the proof for lexicographic path orderings can be modified to a proof of the corresponding result for recursive path orderings.   The paper is a highly sophisticated application of proof theoretic means in the sense of analyzing the structure of proofs.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1899143$0ABC22B3-574D-4C06-8AC3-C1F2E48B5E0A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1899143$E440FF4F-ADAD-4D8C-950E-474EC9B246AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1899143$CB80C8C7-37A3-4C52-9591-67BA1D2F0FA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"23ceee6d3c7c93830578b552513a944677a835cb","datavalue":{"value":"03F15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1899143$51AF3A22-838A-49C9-B7C7-E81CA478511F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1899143$BA89BC5A-E29A-4EB7-B746-252CBC56FC3D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"25c78a8efd68c0736894e7cf9e02e98fcd33b4f5","datavalue":{"value":"802547","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1899143$6E3A831A-80B5-410A-8B65-A8D5DC20082B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c1c662b644cf3bfb15ff11ba35b40c3bbf14ec7","datavalue":{"value":"order type","type":"string"},"datatype":"string"},"type":"statement","id":"Q1899143$01256032-59F5-46FB-8629-09CA6D805847","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"08cbe773d53a3a46b1a097e403df24991b33bbc6","datavalue":{"value":"termination ordering","type":"string"},"datatype":"string"},"type":"statement","id":"Q1899143$FDEF7156-644A-4374-88E2-7FAF860AB980","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"845eb40ab26bf9511aec0526f3a96a0694a29009","datavalue":{"value":"lengths of reduction sequences","type":"string"},"datatype":"string"},"type":"statement","id":"Q1899143$290EF2B1-E231-4417-AB07-4C4010874980","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2937b973c91d3b5515ba93a4c99f71fc3b17f60d","datavalue":{"value":"rewrite system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1899143$C9B20C25-826F-4E5E-A129-C843920B5B50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f976bf826de3b899f73b2f389c1193e0a32f8a0d","datavalue":{"value":"multiset path ordering","type":"string"},"datatype":"string"},"type":"statement","id":"Q1899143$67B79C3B-6E7A-41D8-A0ED-2B361BA6FF56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"34a351094f7879a19220dd10e918894a3211b5bd","datavalue":{"value":"lexicographic path ordering","type":"string"},"datatype":"string"},"type":"statement","id":"Q1899143$4727F1AF-7D37-4BBB-97AD-24054939A1EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f78ff9a60b74189b2daec43f91e02e6e79fb14f9","datavalue":{"value":"well-foundedness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1899143$84434695-3B41-48F0-9503-A919EB1AA651","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"0580dd4129e5d6439921b513d45494c072f33534","datavalue":{"value":{"entity-type":"item","numeric-id":1288968,"id":"Q1288968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1899143$4030D614-9EE5-4E75-A335-9D0446376836","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1899143$0049BA33-35D2-4A4B-966D-4A7D22E78A3A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e01ab232689e474d11c8bd3c944bdcbea19ce97c","datavalue":{"value":"https://doi.org/10.1016/0168-0072(94)00056-9","type":"string"},"datatype":"url"},"type":"statement","id":"Q1899143$DE3A0C74-59EA-44C6-84E7-3F33F8CE8BA6","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"78379d9794d98792f98a6bd739e7ee666f16a7be","datavalue":{"value":"W1968714331","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1899143$77DC875C-6711-4160-BDDA-73AE4C552BC9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e523a40db7b16127f2f0d9abaa913b6b9ced2bc3","datavalue":{"value":{"entity-type":"item","numeric-id":1182465,"id":"Q1182465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1899143$31D8E6D9-A25E-4DA0-AEC1-ABCFCF3AC2E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"173eb0ca706b90c3f5e98576319b1aac6f73c7d3","datavalue":{"value":{"entity-type":"item","numeric-id":3138831,"id":"Q3138831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1899143$A57A144B-5524-4D80-89C8-E08683B29D16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70ecd282533f72abe85687585b23b01adf6e1cf0","datavalue":{"value":{"entity-type":"item","numeric-id":5096206,"id":"Q5096206"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1899143$127F7F07-4111-482B-8476-9C5532E8F08B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05e2a112510c4213854ba517e180e9758ba8b52c","datavalue":{"value":{"entity-type":"item","numeric-id":3960847,"id":"Q3960847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1899143$52F534AB-7073-48AA-A9DB-7BDA9EC2D7BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e8f5bf3bbbb90d2771a6bc1a5bd5d42d5f4b4df","datavalue":{"value":{"entity-type":"item","numeric-id":673975,"id":"Q673975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1899143$95C72301-1C36-47E8-BACF-A6F192C2C4C6","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d15dd14431aad79c0ec12bc08e552b2fb5290bbd","datavalue":{"value":{"entity-type":"item","numeric-id":673975,"id":"Q673975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"11434e21150b5ab7d0c3b1dfd1320acb82433620","datavalue":{"value":{"amount":"+0.8329872","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1899143$C352249B-D16E-492C-A1A9-7D7BFFCE9672","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"07ff1fb2751727afffb0d7607de020c9fece5b4b","datavalue":{"value":{"entity-type":"item","numeric-id":5096206,"id":"Q5096206"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a19134b381bdee1a393e0aad3037dbd67feeef58","datavalue":{"value":{"amount":"+0.8069265","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1899143$FDBFFE3F-735B-4063-A9E7-787A63709435","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d253e9e936bf23eae9d445d2a82c7ce17c22ae5","datavalue":{"value":{"entity-type":"item","numeric-id":1198005,"id":"Q1198005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"09e9def53e8510b0c0584cc36c232e835ec00799","datavalue":{"value":{"amount":"+0.7991563","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1899143$B9CD8EE1-633F-436A-9B8F-28728B41A55F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6385d4a95c988267a30b98baae30830dc6d1315d","datavalue":{"value":{"entity-type":"item","numeric-id":1200982,"id":"Q1200982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd4bbc3eae2416670748f17fcb4a8b372d2bac00","datavalue":{"value":{"amount":"+0.7953242","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1899143$90B76F0A-DBA7-446D-BBC0-B6E901E458EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ca11dce24368e3c4885f53574edd13f932e54a5","datavalue":{"value":{"entity-type":"item","numeric-id":4447240,"id":"Q4447240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f78f39d680e6de3d535ef157d8fd34c86cfa2205","datavalue":{"value":{"amount":"+0.78845066","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1899143$AF306577-91AE-480B-A6EE-A37CCF6AFB53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"712ca67f92282d0a546c8e6fc3e426d1727f3909","datavalue":{"value":{"entity-type":"item","numeric-id":4537515,"id":"Q4537515"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e48e5fdcb267e97552eea386be2128a23ee57c49","datavalue":{"value":{"amount":"+0.78607583","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1899143$8DBFA719-5137-4479-83EC-BF2834E56CB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d55e03f6a9d975c06c4bcf0952bb70c2231d6ea6","datavalue":{"value":{"entity-type":"item","numeric-id":5958622,"id":"Q5958622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cad17ba810325b575cb296fcab154bca228d7587","datavalue":{"value":{"amount":"+0.7817689","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1899143$9C11D685-D547-4AD8-B7C9-D62E836132A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ea089901fddc1de9ab687f8b8630b13dd7ab8901","datavalue":{"value":{"entity-type":"item","numeric-id":4541806,"id":"Q4541806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"655e9ed202c4ee3594c651bb3f0c54e95bbfb723","datavalue":{"value":{"amount":"+0.7799431","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1899143$73A162B7-CC7C-4152-B5CC-12AE4CC0E706","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d6472e09bc9d914d8cab37208ad74013f36ef11a","datavalue":{"value":{"entity-type":"item","numeric-id":1912706,"id":"Q1912706"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"00d18a921caba440f405f24cc14da3b7ebcf37fe","datavalue":{"value":{"amount":"+0.76994616","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1899143$B2D30DB5-A438-4AD2-A271-8C513E7F40B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a131c71e76eddfd40c0ecb8e8ead92f9e2fdc410","datavalue":{"value":{"entity-type":"item","numeric-id":4202962,"id":"Q4202962"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cc27e6dc4d0c025fa0673a1bf7b0ddedb53ac969","datavalue":{"value":{"amount":"+0.7689433","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1899143$77D6E06F-CC1C-46C5-A6B6-32D1EC080B80","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1899143","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1899143"}}}}}