{"entities":{"Q1323317":{"pageid":1334067,"ns":120,"title":"Item:Q1323317","lastrevid":67174737,"modified":"2026-04-12T15:47:38Z","type":"item","id":"Q1323317","labels":{"en":{"language":"en","value":"Proving termination of (conditional) rewrite systems. A semantic approach"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 567287"}},"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":"Q1323317$EE4A6C16-E500-4F21-B5A1-4DB11E5DCEC8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"be7647d09ea948ad18bb0389ffda807611600a84","datavalue":{"value":{"text":"Proving termination of (conditional) rewrite systems. A semantic approach","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1323317$F6F7F5BE-0B8B-4E12-BCB5-D003FA39ADC9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5ada311635072a0cd6ec8f01e039a0599afb15ed","datavalue":{"value":"0790.68054","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1323317$879537F8-1C47-48A6-AF60-353499C47765","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"24099f932a919279e6c40583f21135a4969dbc66","datavalue":{"value":"10.1007/BF01209624","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1323317$3D3C19CD-11FA-47DE-8B16-C799DAF25187","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"32d1f06f1cf8279a92805a6a5735e1b231e8496e","datavalue":{"value":{"entity-type":"item","numeric-id":1323315,"id":"Q1323315"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$7C023585-8263-49FF-94BF-448B0FCD532B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5f18459558c2a64563a14a4617d308f7b62ceb1e","datavalue":{"value":{"entity-type":"item","numeric-id":1323316,"id":"Q1323316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$583AB152-E98B-4950-A4A9-9C7214C03F82","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7d0f02e85530cd06ceb2c58a40dc9c2e0258e194","datavalue":{"value":{"entity-type":"item","numeric-id":161641,"id":"Q161641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$64A3E87E-FCB4-4D5F-9A0D-3C774CA35C1D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2eea7eb210317162e8ade44c06f241e090fd5838","datavalue":{"value":{"time":"+1994-05-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1323317$96B23218-7DD4-4AF5-90C9-2D1DA46BFA89","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"7c706e81572650bff377fabcdd5989df3df17f4c","datavalue":{"value":"An important problem in the domain of term rewriting, the termination of (conditional) rewrite systems, is dealt with. We show that in many applications, well-founded orderings on terms which only make use of syntactic information of a rewrite system \\(R\\), do not suffice for proving termination of \\(R\\). Indeed sometimes semantic information is needed to orient a rewrite rule. Therefore we integrate a semantic interpretation of rewrite systems and terms into a well-founded ordering on terms: the notion of semantic ordering is the first main contribution of this paper. The use and usefulness of the semantic ordering in proving termination is illustrated by means of some realistic examples.   Furthermore, the concept of semantic information induces a novel approach for proving termination in conditional rewrite systems. The idea is to employ not only semantic information contained in the terms that are to be compared, but also extra (semantic) information contained in the premiss of the conditional equation in which the terms appear. This leads to our second contribution in the termination problem area: the notion of contextual ordering and contextual semantic ordering. The contextual approach allows to prove termination of conditional rewrite systems where all classical partial orderings would fail.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1323317$927526F0-2E0A-433E-B361-A637CB882E9D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1323317$BA176AFD-DB0F-431E-9B8D-3FE93D29F5AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1323317$961618C0-791C-4364-B2F6-91DF4CCAB5F6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"34bb73d92c2fa452dcc1af9932f49270fb33d401","datavalue":{"value":"567287","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1323317$1F63FE39-FE58-4E0A-A4E1-82C116F83E22","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5a664fc87eb2216b1fad976387dcf6ff589b12b5","datavalue":{"value":"term rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q1323317$13BA4A29-95A4-49CD-888F-A8DA4A5045A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4befa4ca20f2beabcfa09e8a92ae13c21cb4934a","datavalue":{"value":"termination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1323317$C0B7F0B6-F2EA-4C19-9F2C-C22000D1AFCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e1e162b6480412c2f5494c42b815c6e1b7024b54","datavalue":{"value":"semantic ordering","type":"string"},"datatype":"string"},"type":"statement","id":"Q1323317$A9DA2922-7C38-419F-B30D-C7AA147B47B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cd708a876b7b3663e130383f34c2d5381f308f20","datavalue":{"value":"semantic information","type":"string"},"datatype":"string"},"type":"statement","id":"Q1323317$08F42866-13C8-4825-AE29-B24AFFD2FFAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"65cffcc10d54ff11d0211f73a77cfac651762fa3","datavalue":{"value":"conditional rewrite systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1323317$D45D2500-EEFE-4583-95D2-5F5077FB1BC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"54fa4a508e5890e5e657c6c71f49500ef249b429","datavalue":{"value":"contextual ordering","type":"string"},"datatype":"string"},"type":"statement","id":"Q1323317$72BAED6B-58C4-435C-9D17-EE934EA7A725","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cdc09159c3d9e35e53ef549059a47b095580c647","datavalue":{"value":{"entity-type":"item","numeric-id":40621,"id":"Q40621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$5B311C4A-2C4C-4916-88B5-7939CCE36C53","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":"Q1323317$3FEBB6FC-3605-4B69-AEC9-1DE9E4B24BAE","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"39fbadb486268c409587b62af0d1cffcf61437d4","datavalue":{"value":{"entity-type":"item","numeric-id":3484358,"id":"Q3484358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$7B890D28-4339-4024-A72C-D561AFF97E1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e68522e480793ad08c3035e092f5d824e5fae6d","datavalue":{"value":{"entity-type":"item","numeric-id":3783521,"id":"Q3783521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$39120A01-4158-48E5-98D9-4E560E6CF1E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"59bb3344b4f89870291c44462654819d8a7d7295","datavalue":{"value":{"entity-type":"item","numeric-id":3809306,"id":"Q3809306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$7BD45FD4-4491-4C84-AF03-F84474085379","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f679ec815734356302ea7e28b648fb1eb1701bc0","datavalue":{"value":{"entity-type":"item","numeric-id":3757390,"id":"Q3757390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$98297335-D850-472C-9109-64348CE2387C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30bcadb47052699537df970445bd0e9b5b4dbb7d","datavalue":{"value":{"entity-type":"item","numeric-id":3783523,"id":"Q3783523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$5179BEAA-D80D-4D8B-8FFE-26109BAC1996","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"612e9cb9341b02f6944a85a1a0388d9d9a0f8994","datavalue":{"value":{"entity-type":"item","numeric-id":579930,"id":"Q579930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$96939A34-466F-4004-ABBB-3A5FCE4881D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a03dacafad2ff19ded175ac7d62381d002687606","datavalue":{"value":{"entity-type":"item","numeric-id":1111368,"id":"Q1111368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$D4EB4FA6-8A87-46A6-971E-799C1BFC701C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8124e2aa86067094dab23bb14b8dadf2e19d522b","datavalue":{"value":{"entity-type":"item","numeric-id":3894958,"id":"Q3894958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$D164E293-8C04-4918-A637-ECFBF97F0853","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab8ea372caa817f188e4e943a4cbc2ab55cc9d12","datavalue":{"value":{"entity-type":"item","numeric-id":5549412,"id":"Q5549412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$93689A9A-1D35-49A0-A532-AD33697F388E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e5985ede7bd580a3b6a10ed6c28ef50e7923f93","datavalue":{"value":{"entity-type":"item","numeric-id":3819993,"id":"Q3819993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$D79C39D5-549B-4A93-99D4-04BB7441FF8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e0f4147474a7e5a4baf84f193c7501316743b5b5","datavalue":{"value":{"entity-type":"item","numeric-id":1139374,"id":"Q1139374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$C2A68BED-3C03-448F-9479-E25BBDCFAB99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"378088a63ec20245823db74d6a8845609e39ce21","datavalue":{"value":{"entity-type":"item","numeric-id":593789,"id":"Q593789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$84558BB1-1AA0-46E6-93F6-478E15BC1B78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d6d3f5f0e6d39b0610560c479018fc71a2adcd20","datavalue":{"value":{"entity-type":"item","numeric-id":1098624,"id":"Q1098624"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$B5A178F5-B280-465E-AF50-E7ABBC7C1038","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91fe9fac1d5e9172bf0ce58a41176ff7a486982b","datavalue":{"value":{"entity-type":"item","numeric-id":1187660,"id":"Q1187660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$526353D7-78CA-4B3A-A6A9-E309F14DD066","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a01d4a91dcf05e247efe3d36d8b1cf5c4792f88","datavalue":{"value":{"entity-type":"item","numeric-id":4385532,"id":"Q4385532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$CD844277-6F61-4ADB-B8CA-614AF52A0073","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"89e6b612eb3cb0e65ff83e8cd8762940dc520785","datavalue":{"value":{"entity-type":"item","numeric-id":3659124,"id":"Q3659124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$EDF1A507-D8E9-40BE-8F96-CA22393B65D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de9f23bc58febcc60aff99ac387949cd328d3079","datavalue":{"value":{"entity-type":"item","numeric-id":1065790,"id":"Q1065790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$615DBDD2-90C8-46CC-9AD1-E3B5733565D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc38d5f7a802e9ea35c5abdf22fc0003a899e4fd","datavalue":{"value":{"entity-type":"item","numeric-id":1100891,"id":"Q1100891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$715E7F1F-9534-4486-B27C-374F031D6E95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"108976005e438ca70f7496d07e6faca25fa804e7","datavalue":{"value":{"entity-type":"item","numeric-id":3683533,"id":"Q3683533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$CBA4F544-255B-4C91-86AD-F96D827E4D67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1e0b4fc54e8c62a86959e50d4b1b27d9d9a092c","datavalue":{"value":{"entity-type":"item","numeric-id":5581665,"id":"Q5581665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$D5C57CC3-FBB0-4BAA-AD3E-D1BB8852D822","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ee7b430836cd50b9ff8b1b508fe37ed305a1d07e","datavalue":{"value":{"entity-type":"item","numeric-id":3336681,"id":"Q3336681"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$2080C808-F5FF-43A1-B459-EDEF9366532D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ad4a5c557927a71dba39dcd7727faf63d604bad","datavalue":{"value":{"entity-type":"item","numeric-id":912609,"id":"Q912609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$8A5634A8-7702-43EE-98BC-77F53764E372","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a664fcd7d41eeb4ed77ef9a598d8a6631479e23a","datavalue":{"value":{"entity-type":"item","numeric-id":3779786,"id":"Q3779786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$95759077-9ECB-4B7B-B25E-4C05213C4181","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c532246ad2110361bfafa9cb26e4c54d1d686bf1","datavalue":{"value":{"entity-type":"item","numeric-id":3696501,"id":"Q3696501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$7C430774-E01E-4FBE-A273-1CF5E29C3A8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4c644393292b3f41469d648371f2669fdfbbd2a","datavalue":{"value":{"entity-type":"item","numeric-id":3805961,"id":"Q3805961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1323317$F2FB153D-0C12-47FC-9A19-94267AE6D44C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"578000072a60f0b4b8705359c25342662b6437b1","datavalue":{"value":"https://doi.org/10.1007/bf01209624","type":"string"},"datatype":"url"},"type":"statement","id":"Q1323317$819141F7-591C-47A0-A0F2-F0DE6D8D21A4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4add0ee723703e40fbb517f952f8915344db1864","datavalue":{"value":"W2911610589","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1323317$DD619909-1634-4C43-8A62-B370A42DCFD1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"35398bb68961ca6ca6005a2a56e2e38acea57fa8","datavalue":{"value":{"entity-type":"item","numeric-id":3703288,"id":"Q3703288"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"938b3b49445f0ffa30ebd25cf947b3dc5cb6a82f","datavalue":{"value":{"amount":"+0.822624921798706","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1323317$A049D280-77EC-4D80-9D28-ECBE6751AB09","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":"aeb8219bb28d19c7e1039fddae97596e411e1863","datavalue":{"value":{"amount":"+0.8221232891082764","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1323317$361E0A4E-055B-45FF-98DB-679A7FC7A6AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bea7c6583cfd2b84f9afe3601a34770b09886021","datavalue":{"value":{"entity-type":"item","numeric-id":1332336,"id":"Q1332336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"147ac2f423ce7abe360ba9c3f3164ea6460d4376","datavalue":{"value":{"amount":"+0.8109468221664429","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1323317$8CA048DB-D75F-450B-BF91-580C83F4147E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proving termination of (conditional) rewrite systems. A semantic approach","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proving_termination_of_(conditional)_rewrite_systems._A_semantic_approach"}}}}}