{"entities":{"Q40298":{"pageid":40354,"ns":120,"title":"Item:Q40298","lastrevid":105426950,"modified":"2026-10-09T10:06:30Z","type":"item","id":"Q40298","labels":{"en":{"language":"en","value":"Knuth Bendix Orders"}},"descriptions":{"en":{"language":"en","value":"AFP entry Lambda_Free_KBOs"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"26d9845293bc8ee93ac052600fff056cf5bae5a0","datavalue":{"value":"28584","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40298$E8C5124B-8BF5-4ED3-AE3B-B0B12C90A944","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":"Q40298$FB3F1B48-10D6-4F7E-94A1-C6F499A059BB","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"f0518268a7ed95826152df21d63b4529cefa6e22","datavalue":{"value":"https://www.isa-afp.org/entries/Lambda_Free_KBOs.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40298$E9C561F7-9DC0-488B-AC64-3E24616BA889","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40298$42E0F438-560A-4581-A2C3-573C20E64213","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40298$583898A3-4193-4B58-875B-408E9D81CB20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40298$265AD662-4CF5-41B0-A5CB-E32F21B5345F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40298$5DAC0637-68F1-45F4-99C5-184C93736CD0","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8dde418bf28e22fefe1976bd953eb7c8ec5b548d","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$809C900E-B533-4B97-9DBB-022BF0968495","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$5663E28F-C3C0-4AFD-9EE5-04B81A654B3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"937a19baf3283c91e89f0a08dd8e59bb640da883","datavalue":{"value":{"entity-type":"item","numeric-id":40624,"id":"Q40624"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$25A32ABB-4C0D-432F-926D-5E9641DBDE7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$20423C03-E7ED-4289-89BE-AC75365752EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a453efbcf3d9ea5b4f1cf5afc4278b60c86ae43d","datavalue":{"value":{"entity-type":"item","numeric-id":40506,"id":"Q40506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$22998445-2DB1-422E-8272-7DD1A94D9C6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"331995fe532c23e24d72d01a1bd6245fafcd9671","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$7363182F-07D7-48F4-8BCD-BF2BD6E0093A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8bf2731143fd82a1f95f40f13b2fce56fbb7345a","datavalue":{"value":{"entity-type":"item","numeric-id":40299,"id":"Q40299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$EDF1312C-ED35-45E6-A748-24B437D78565","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f70e8f897325b539c702d8d7cb97dfafe554224c","datavalue":{"value":{"entity-type":"item","numeric-id":32823,"id":"Q32823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$3F96F178-D24B-4816-961D-F245885A2DF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9ad8338290e864661fc95f2a66261cf7e07a407c","datavalue":{"value":{"entity-type":"item","numeric-id":32822,"id":"Q32822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$05FB67EE-9C0D-4743-959E-BE7020102120","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"e5e8684e8339ba421338afd59297e657343b949d","datavalue":{"value":{"entity-type":"item","numeric-id":21785,"id":"Q21785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$6C48BC73-AF3E-48EF-873C-F316E2BFE18D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1f35d67f190b2d0ea091b0b9c5f82f92823c75e9","datavalue":{"value":{"entity-type":"item","numeric-id":19136,"id":"Q19136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$2B05B877-73A3-4F63-AE53-121EB56E610B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2fd4f2f31989858180fba533a04e1a60c8d16377","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$BE1F0A49-31D3-47D5-9705-9A749E441EC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f1bbc3872a55b3dfa074c96d37fd46f076f92caa","datavalue":{"value":{"entity-type":"item","numeric-id":24736,"id":"Q24736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$09CB5416-79F5-4671-84BB-55E36F2E9A02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"493c5144a9d14f0b980d45769fb4b197b51b453c","datavalue":{"value":{"entity-type":"item","numeric-id":40555,"id":"Q40555"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$32CEC815-A37A-4B88-BE83-BCAA1C62DB84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"37701d360bad336addd4a826712aca6608c48c21","datavalue":{"value":{"entity-type":"item","numeric-id":40554,"id":"Q40554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$91FA4A34-A9CE-4F55-973D-24FBADBDD7DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b677ab36580483ca33e96c40f998e187dadaa8b2","datavalue":{"value":{"entity-type":"item","numeric-id":40553,"id":"Q40553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$F7FFA654-87DC-4215-8CB1-CF1F2DD086A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"861e34f6b532f04d877297070a58fb137923d509","datavalue":{"value":{"entity-type":"item","numeric-id":40509,"id":"Q40509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$6AD5FAD9-E11D-4272-8F5A-170E874EEC72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"5a186263bc9fb77c5d68f5852fbf845cc855223a","datavalue":{"value":{"entity-type":"item","numeric-id":40326,"id":"Q40326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$50F6B726-3B6E-4BA5-8A8F-993B90448FE9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e8e296a30b9cb4881038eafb44c48ebfb57df361","datavalue":{"value":"https://isa-afp.org/entries/Lambda_Free_KBOs.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40298$D2739B0F-21C9-4C93-85B4-46BD9AD69D2E","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"cb22bf99c25c82624daeee7c7a8b4cf253d85a7d","datavalue":{"value":"Heiko Becker","type":"string"},"datatype":"string"},"type":"statement","id":"Q40298$DD98FC25-3EF8-4DDE-BCAA-FCB8C1262ABD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"d593b6f197721b1ecf9f17d8e5bbb2bb5a1f7f8a","datavalue":{"value":"Jasmin Christian Blanchette","type":"string"},"datatype":"string"},"type":"statement","id":"Q40298$ECC87BA3-CFFE-4EF6-BD1C-1AB765EA3622","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"0bea28856612bb879f597a9d9f573ece274a0783","datavalue":{"value":"Uwe Waldmann","type":"string"},"datatype":"string"},"type":"statement","id":"Q40298$7D9ED310-72B2-4699-8CC8-9C84D018F8C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"8a2e470a50e057f2285d5354789df0be451a8ef1","datavalue":{"value":"Daniel Wand","type":"string"},"datatype":"string"},"type":"statement","id":"Q40298$046DBBD6-C06F-42F0-B015-1758D8F7D21D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"796efb4179e2ca35d0af5275cea4f55df2a458b8","datavalue":{"value":"This Isabelle/HOL formalization defines Knuth\u2013Bendix orders for higher-order terms without lambda-abstraction and proves many useful properties about them. The main order fully coincides with the standard transfinite KBO with subterm coefficients on first-order terms. It appears promising as the basis of a higher-order superposition calculus.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40298$E80F5317-8AF8-49A4-97AC-B613CA737AA6","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"cd0c9d6eaf2232ef6bd24acb440211c3c1735214","datavalue":{"value":{"entity-type":"item","numeric-id":7361192,"id":"Q7361192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$E23FDAA6-0A3D-421E-BBA3-C5DB8B0AEAC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"8f0f13c41ff97fc90cd117120ced19e3dd24a1b3","datavalue":{"value":{"entity-type":"item","numeric-id":7361305,"id":"Q7361305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$974F9E75-B387-42FF-8662-18977B8049D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"3083b28cc1bd9860f5bb551df5db6c97e7a4c0c4","datavalue":{"value":{"entity-type":"item","numeric-id":7361593,"id":"Q7361593"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$2AF61DBF-F868-429F-AA02-429C27A678EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"a0e462408f240420e2b3f4dd5e025dcac9e4a9cd","datavalue":{"value":{"entity-type":"item","numeric-id":7361044,"id":"Q7361044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40298$CC5D9E7A-4467-4B7C-9F1A-CF9A7FBEAEE2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"41ff541fd86139b491ded56d8988e9c4cc3f5963","datavalue":{"value":{"time":"+2016-11-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40298$057CCA56-DC26-4179-BB1C-E02614AED3EE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e923215a66189e773fb55d42ffb21ab81409e479","datavalue":{"value":{"text":"Formalization of Knuth\u2013Bendix Orders for Lambda-Free Higher-Order Terms","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40298$2609DAE4-36F5-434D-8DD9-708ADA8F09DD","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":"Q40298$3257FC7A-9C2B-4A14-BA63-FB0EEA0BF36D","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":"Q40298$53D47EE9-B6BF-4071-8AAD-C0EEFCB3B6A7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Knuth Bendix Orders","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Knuth_Bendix_Orders"}}}}}