{"entities":{"Q843949":{"pageid":845797,"ns":120,"title":"Item:Q843949","lastrevid":64762761,"modified":"2026-04-11T22:03:40Z","type":"item","id":"Q843949","labels":{"en":{"language":"en","value":"Coq formalization of the higher-order recursive path ordering"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5659684"}},"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":"Q843949$BE99BD05-F509-463F-8312-8E13C223E62E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4c002096055e9db8a57f8d85069252fed625f758","datavalue":{"value":{"text":"Coq formalization of the higher-order recursive path ordering","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q843949$D7C80DE3-23CC-4496-B84A-014CA4758D2D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"286c529d3c006fe4548bc9227de21547e909801f","datavalue":{"value":"1185.68628","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843949$E524ACAA-19F4-4F71-914A-F6BD0E8E6CB2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b43147a09f38888bdc440722fa90e825a1545dbf","datavalue":{"value":{"entity-type":"item","numeric-id":843948,"id":"Q843948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$17651998-1D0B-4F93-A2F9-D87A7CD8B194","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e71b1a810c94176f33b214acd409208085d409e4","datavalue":{"value":{"entity-type":"item","numeric-id":162945,"id":"Q162945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$6F4105EF-4BA8-4DAB-9E9D-C3A2B39B1944","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"160ae7be62905e153a649a9a4d09ab3aa02ded62","datavalue":{"value":{"time":"+2010-01-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q843949$0EBEF6A6-2A80-4733-9A1D-AB773D49EB55","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843949$944EE41A-A585-4941-84B8-4E7A9DEADD69","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0b53dfdb56b8989b3b0e45edd89efee15f054c5c","datavalue":{"value":"5659684","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843949$26460706-1102-49DB-8995-7372C027B3DD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q843949$0314FA8A-8ACD-4202-877F-3FA0249E08C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d32d0aa051e0e2d718d1b62470aabd2c380221b","datavalue":{"value":"HORPO","type":"string"},"datatype":"string"},"type":"statement","id":"Q843949$FDB5793D-383E-4E16-B6E9-F8A0C2C2FE70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"02fe2537e5a6a19502e9e8c005da353bb805a871","datavalue":{"value":"Higher-order rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q843949$12B8804B-3E49-4C75-8B82-8A22DF141D30","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$7CA889BC-C0C1-4C8B-BB3A-1AB55382DF77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$8768E960-3228-41ED-A5C0-180D9A6901B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e916eb1dc395e3830d6317d3e8aefcb052d11440","datavalue":{"value":{"entity-type":"item","numeric-id":21785,"id":"Q21785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$B411D811-3CD7-4B0E-9EA3-9A98634174CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8be5ee5254d2a781e0ec7bc0b35265c3f1813a9a","datavalue":{"value":{"entity-type":"item","numeric-id":22078,"id":"Q22078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$D3392611-5841-4648-AEFB-46C5EBB85632","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":"Q843949$3A284E3F-F39E-4674-B86E-73686558B2D6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"14efd02425b2f9eb5d16cc418cbc61a86a81bc81","datavalue":{"value":"https://doi.org/10.1007/s00200-009-0105-5","type":"string"},"datatype":"url"},"type":"statement","id":"Q843949$293F9387-DD69-4F3E-B4E5-F224BBC0805A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ea666ac010d95a914616c28e095aebca47e0331c","datavalue":{"value":"W1998337489","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843949$B889CD5E-AC8A-4456-B339-88EB29A5DB6A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d8bfe191ca90d3395347096033dd0a0643030e0","datavalue":{"value":{"entity-type":"item","numeric-id":4281462,"id":"Q4281462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$3759ACAF-8B6A-4C4C-821C-9C273ADA763B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79ce8544fc5a0489695eae9a558cb4d34b573281","datavalue":{"value":{"entity-type":"item","numeric-id":5477646,"id":"Q5477646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$6B7C97CE-F47B-4C2A-9A3D-A0CC317E613F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"819a2535befb2a67f49ee5e43432525215be36de","datavalue":{"value":{"entity-type":"item","numeric-id":4702972,"id":"Q4702972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$26F3B7D0-570B-4739-8D1D-8CEDFF303020","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8497b2d78ba0b1939b3cc4392136c45f636c16c","datavalue":{"value":{"entity-type":"item","numeric-id":817701,"id":"Q817701"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$3F062E0A-08D9-4FD9-BBEB-D6340ADCBBC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eeddfec2d6761bcca5b706cfa4f21836083ab429","datavalue":{"value":{"entity-type":"item","numeric-id":5712322,"id":"Q5712322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$EE240433-30E4-4CB9-9248-058D936F3A51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$E16A9BC2-0A97-4CF5-BF99-F306FFAA17D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"87641d285819518c18aad91a7f60b475458b9f24","datavalue":{"value":{"entity-type":"item","numeric-id":3498461,"id":"Q3498461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$53914090-897F-406A-8F59-A342C9F987C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70d5dcacdf82491509f047ffa7adf630e71ade90","datavalue":{"value":{"entity-type":"item","numeric-id":5667469,"id":"Q5667469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$9AA46125-4AB9-4E1A-9ABB-922E8C7BAC2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca7e027091589776f78a6d7ad8457e805c17b28","datavalue":{"value":{"entity-type":"item","numeric-id":5777498,"id":"Q5777498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$E7BCF48E-557C-4339-ABD8-FCF1A21E525D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec28ba6d820be907a77fb84eda09cc97c627df63","datavalue":{"value":{"entity-type":"item","numeric-id":3525007,"id":"Q3525007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$0B0A9DDF-0561-4ADE-B2BD-D807EC82CEDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0af54424d73601bfe92d71557c46e9093990ffc9","datavalue":{"value":{"entity-type":"item","numeric-id":857884,"id":"Q857884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$66077DEF-EF87-445D-BF4D-962F320EEA55","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":"Q843949$E5DE9494-49C0-4E14-B051-30312FFC417F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61fde8a68f7ac705939927db78446d9cd7abd767","datavalue":{"value":{"entity-type":"item","numeric-id":1182475,"id":"Q1182475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$D0B42E46-8C46-48A0-9989-E179BD3F646E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99c6176bcb92cea3bde43c51d54f8875f446d09c","datavalue":{"value":{"entity-type":"item","numeric-id":3994895,"id":"Q3994895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$625FEFF2-1838-4341-B11A-5F5496171529","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cd22f0cc6d347d0883b044bb9468db1ab7dd5a3b","datavalue":{"value":{"entity-type":"item","numeric-id":4346206,"id":"Q4346206"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$143492E3-07FD-4914-A753-E723C08669FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da79663fa6c445059603456269c9902280a33779","datavalue":{"value":{"entity-type":"item","numeric-id":3546327,"id":"Q3546327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$3F2B510A-8BD0-486C-B358-3ECC893F8DB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6476dfd88c72a0f923de2fd86bcd0837d9a7ef7b","datavalue":{"value":{"entity-type":"item","numeric-id":3527310,"id":"Q3527310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$2315C13F-B824-499E-93B7-E8B12EA0FC0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc089b46277af6c6062ec2909ab2c739e53c087d","datavalue":{"value":{"entity-type":"item","numeric-id":3527297,"id":"Q3527297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$9CC22231-826A-4801-B34E-51A59FCF79BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c99e28edfd88bdd97fad0b6f216698f926941cd1","datavalue":{"value":{"entity-type":"item","numeric-id":5448658,"id":"Q5448658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$F4469177-041A-4698-9548-FAE21A2FC638","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e4064b8cefaa1973205852b506694731297b828","datavalue":{"value":{"entity-type":"item","numeric-id":3024845,"id":"Q3024845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$66C6590C-32EF-4419-A358-80155E6613E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf1e6e74fc9f0e43b2bb5ebeafd488ad5919a3c3","datavalue":{"value":{"entity-type":"item","numeric-id":1112816,"id":"Q1112816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$2A866E84-FF20-4F55-8FC2-B546D50F6EC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ddae3cd6c81f3adeb0b414d4377c9d2993c7433","datavalue":{"value":{"entity-type":"item","numeric-id":2852349,"id":"Q2852349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$CE2895E6-9EA6-41BC-9C16-7896BBDBD806","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c7130b8e8ad403bac4e3a609004e5598d1175d3","datavalue":{"value":{"entity-type":"item","numeric-id":5561939,"id":"Q5561939"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$7742F620-CBD3-4A0B-B778-E7D10E38716F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"397e61c05725fd10ade5bdbfed8ada2d720d5480","datavalue":{"value":{"entity-type":"item","numeric-id":2778883,"id":"Q2778883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843949$85BB28B2-8BBE-401E-9E17-D096609228FA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e8a4a67b09ceff1efa629aeb70a2f60c332b8c04","datavalue":{"value":"10.1007/S00200-009-0105-5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843949$42A4A13B-E516-4F0B-974B-D872863DA0E8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12bfe788d3ff49a680b8b0521c90e3a8a7fbcb40","datavalue":{"value":{"entity-type":"item","numeric-id":3527297,"id":"Q3527297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3cda50c29a2ced1cb08b3ea53dba6cae6ab5853f","datavalue":{"value":{"amount":"+0.932824969291687","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":"Q843949$4C8A1CE6-5547-4BE5-A0D0-2AEA621655B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"baf00d78dba38081d710d62187402849bdd55995","datavalue":{"value":{"entity-type":"item","numeric-id":3024845,"id":"Q3024845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64ba348739133a795a67486006a32f55d1d862a5","datavalue":{"value":{"amount":"+0.8356003165245056","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":"Q843949$145C5B98-D0BE-4F4E-9B39-D154D4D70E7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"849c17cb94218e8fed782e07a8b252a384219966","datavalue":{"value":{"entity-type":"item","numeric-id":3196359,"id":"Q3196359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a873ee28e165e40b50178c8990f1cd5e3be2ade0","datavalue":{"value":{"amount":"+0.8264806270599365","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":"Q843949$C1269055-3FF3-454C-865D-AE0C4A3E9359","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b0c61e6fd01e935344860ee668c18458e006fba","datavalue":{"value":{"entity-type":"item","numeric-id":2988386,"id":"Q2988386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"67b8bfb4d5caa4676fae8bf7d8760c30e3bae56d","datavalue":{"value":{"amount":"+0.8173394799232483","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":"Q843949$511F3A22-4EAB-4702-B275-B6E725B71AB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cef9cf6987fdb38041d6207038228071299b8c8d","datavalue":{"value":{"entity-type":"item","numeric-id":3546327,"id":"Q3546327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1a216f73d135f20e70ad8764dfd15eef02abfe40","datavalue":{"value":{"amount":"+0.8164708018302917","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":"Q843949$4ACBA774-8BBB-4863-92C6-7D044D665F60","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Coq formalization of the higher-order recursive path ordering","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Coq_formalization_of_the_higher-order_recursive_path_ordering"}}}}}