{"entities":{"Q1154801":{"pageid":1165550,"ns":120,"title":"Item:Q1154801","lastrevid":69753906,"modified":"2026-04-13T09:09:47Z","type":"item","id":"Q1154801","labels":{"en":{"language":"en","value":"A complete proof of correctness of the Knuth-Bendix completion algorithm"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3729441"}},"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":"Q1154801$A16B4BB0-57BF-4F58-8411-F965B32CB579","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d02dbb760ebee17f24b723136b21a8fd36dd3180","datavalue":{"value":{"text":"A complete proof of correctness of the Knuth-Bendix completion algorithm","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1154801$A2F40623-A04D-4095-9F6F-C28B7E0AEB6C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"56bb84630fe39e9337f4fff14c118ab10e665b88","datavalue":{"value":"0465.68014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1154801$19D03C34-C39B-497C-8CC2-D50AA92395B2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5d5ba93743cc59443673f2d0014fcdc16783055f","datavalue":{"value":"10.1016/0022-0000(81)90002-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1154801$D3E8B3A9-75CA-4FFB-9B1B-BB2EB75E3769","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4f9facad47142ae6aca78e42226d987a134e9bf3","datavalue":{"value":{"entity-type":"item","numeric-id":789175,"id":"Q789175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1154801$99E1998D-836D-4382-AC4B-C268389E85A6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3340243f57e05f2265c56423c388055a14b114fa","datavalue":{"value":{"entity-type":"item","numeric-id":107189,"id":"Q107189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1154801$68C4D7A5-C761-4A08-9541-958A0BB4F258","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"50fad0db7dc87cb4e51866acdb5ccbaa54ec857b","datavalue":{"value":{"time":"+1981-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1154801$D1FF8D75-59B4-45EF-BBBF-ED5279BA188E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"35e14023b9f663ac06b8e7c7730708ebf3d26bbd","datavalue":{"value":"https://hal.inria.fr/inria-00076536/file/RR-0025.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q1154801$5E1CD533-24EF-4DDE-87AD-8CCD00F2550D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ed1e3c6cced595a05b8ae19055521b22405b78a","datavalue":{"value":"68W99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1154801$868B60D2-B224-4EA0-9A05-D43AD0D1F675","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1154801$DC1A3844-2675-4958-99C2-22B72443BA17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6ed618702b057009a2070ae378cd09839bebae6c","datavalue":{"value":"08A99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1154801$908DC288-254C-4E85-9C4C-D842A601E398","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1154801$A04B44E6-1410-4AA7-AFD0-D61BC3097AE0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ac3da15c40c080a254514c74237b21a38d9df69d","datavalue":{"value":"3729441","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1154801$7D745485-5060-4B7B-8D65-352DA4A8060A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"25d573905ca968c131d1a2bab31fb25067e92744","datavalue":{"value":"semidecision algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q1154801$440A10C9-4224-49BC-BFF1-926FE6330AA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dd59e5bee4cef5f69ba8393f3a75f4497e1a2e64","datavalue":{"value":"validity problem in equational theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q1154801$0BBC88E5-E47C-4C23-9698-AF8A08ACD358","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb79299daf8f29391d6c8a2b4222865ffe474551","datavalue":{"value":"decision procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q1154801$75028EFF-3D0E-41A5-8C0F-7AA12F1D94E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5a664fc87eb2216b1fad976387dcf6ff589b12b5","datavalue":{"value":"term rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q1154801$45B55151-943F-4317-B61A-C5EAB4EABE0D","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"3592942b2277b1c2eba0826621d1404bb7c5fd7a","datavalue":{"value":"Q55952378","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1154801$AAC25A03-3C10-422F-BF9A-28BA0B2DD00D","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":"Q1154801$D4F9835F-FA55-45DE-9F59-0532E7A49A96","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4818cf3e1331624c5327cbf40817a3e59f887ddb","datavalue":{"value":"W1991856459","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1154801$5319A8CA-B430-46CD-AB0C-E6814C45E6F5","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e57dada08276bdfd975413149fdc809775588d67","datavalue":{"value":{"entity-type":"item","numeric-id":1147232,"id":"Q1147232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1154801$6939825D-9320-42E6-9DF8-CE40DE29500F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"599c5dbf52817fbbe5f2f15e33a96dc6ac97514e","datavalue":{"value":{"entity-type":"item","numeric-id":3908463,"id":"Q3908463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1154801$4A450D2F-1648-4458-9464-9760BD279F98","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":"Q1154801$6DAFF6FC-3B2C-41E3-B787-E18FAB7F498C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8670a1cb5138f59a7607a06c6c33e9eef7f2c9ea","datavalue":{"value":{"entity-type":"item","numeric-id":3938536,"id":"Q3938536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1154801$3803381C-E304-4580-A85D-F4FB317F78B8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A complete proof of correctness of the Knuth-Bendix completion algorithm","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_complete_proof_of_correctness_of_the_Knuth-Bendix_completion_algorithm"}}}}}