{"entities":{"Q7361077":{"pageid":31518770,"ns":120,"title":"Item:Q7361077","lastrevid":105362594,"modified":"2026-10-07T13:34:22Z","type":"item","id":"Q7361077","labels":{"en":{"language":"en","value":"A Formalization of Knuth\u2013Bendix Orders"}},"descriptions":{"en":{"language":"en","value":"AFP entry Knuth_Bendix_Order"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b1ecbf726df4f9c342fc765ee3332bceff7f7abf","datavalue":{"value":"https://isa-afp.org/entries/Knuth_Bendix_Order.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361077$43C15F86-A847-40A5-9418-3FECED86A53B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6d0c48627b068f854a947856c3807165d49ca3ba","datavalue":{"value":{"time":"+2020-05-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361077$E8BD43C8-EEE7-4810-AAB0-668C908E7749","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7335db8cbac804a8435e80e80636b4dde04d73bd","datavalue":{"value":"Christian Sternagel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361077$86CAFA7C-06FF-43A9-BF78-67F94298B880","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"3e961f1f2b2e533bd88ffdbcd178bd2ef2813f73","datavalue":{"value":"Ren\u00e9 Thiemann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361077$CE62097D-0AFE-4C45-98F5-46725E620A6B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ae9e9f6b09df658208de8e587be317ac17f24e95","datavalue":{"value":{"text":"A Formalization of Knuth\u2013Bendix Orders","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361077$9EFD064F-BA3A-4EFB-815D-513AC6E5D761","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"40c6ace6bac8880acee4b6490ea6119e2642a890","datavalue":{"value":"We define a generalized version of Knuth\u2013Bendix orders, including subterm coefficient functions. For these orders we formalize several properties such as strong normalization, the subterm property, closure properties under substitutions and contexts, as well as ground totality.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361077$7453A859-7187-4AB2-9720-D8FBB88BCF0A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f87d791b3bef9ce142540481bca9b113bf919089","datavalue":{"value":{"entity-type":"item","numeric-id":751830,"id":"Q751830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361077$A16A03B7-E123-4AB6-8D79-4DDC6ADE16FA","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":"Q7361077$8157F75D-0D3F-4F23-A216-0AF23314B489","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8fe753357a6d82c52967f1976a05f5e36a3cab5a","datavalue":{"value":{"entity-type":"item","numeric-id":3498479,"id":"Q3498479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361077$F19377ED-CCB3-4224-B637-659B503D40AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b6a03213b095a350f4bf2d8dc4d804066ee4390f","datavalue":{"value":{"entity-type":"item","numeric-id":2958390,"id":"Q2958390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361077$B4EFBBE1-E8D6-44AF-A874-3129190844A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f29b3c236e91c30852d16d4ed27cc41f72168feb","datavalue":{"value":{"entity-type":"item","numeric-id":5055737,"id":"Q5055737"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361077$D9FCC2BD-B3E5-43F4-B7D0-5C58010A2564","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0aef60bd392ccfb5e82daa98f095917b33d1745","datavalue":{"value":{"entity-type":"item","numeric-id":3183545,"id":"Q3183545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361077$D5AD1E34-B094-4914-BF95-C826DE62FE9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a77128970ef1ae7664b1eef0de5f0b57e43899ac","datavalue":{"value":{"entity-type":"item","numeric-id":846165,"id":"Q846165"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361077$46A75D0D-A2A8-41F1-B705-F14F29F17249","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361077$228A17D0-17FB-4723-84D3-BAD49689E4A7","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"6d228da4bce2fba997fec5a975b2ba853633b29e","datavalue":{"value":{"entity-type":"item","numeric-id":7361840,"id":"Q7361840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361077$CC1FF295-27DC-4ABF-A525-FBBCE3AABE74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"911ce259dbcadd322bcb1b83dc5bfce4b6c36b1b","datavalue":{"value":{"entity-type":"item","numeric-id":7361212,"id":"Q7361212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361077$42754C62-C1B3-4376-ABA0-B8D63F05D0A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"0c9c9f0c4eee9c4734b6223c2dd6a0c94c9a6581","datavalue":{"value":{"entity-type":"item","numeric-id":7361085,"id":"Q7361085"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361077$02C9E8D1-A97B-42F2-B724-D29B7BC2B860","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"edf8a8949edec3767dd80b6d3acecc92e5d25f1c","datavalue":{"value":{"entity-type":"item","numeric-id":7360818,"id":"Q7360818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361077$5C8456AD-539C-43CB-95B2-02BA4AA38478","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361077$D160A0BE-4E19-43BF-B92F-A947BAB9BB0B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Formalization of Knuth\u2013Bendix Orders","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Formalization_of_Knuth%E2%80%93Bendix_Orders"}}}}}