{"entities":{"Q2829265":{"pageid":2840003,"ns":120,"title":"Item:Q2829265","lastrevid":52660109,"modified":"2026-01-23T05:18:38Z","type":"item","id":"Q2829265","labels":{"en":{"language":"en","value":"Automatic functional correctness proofs for functional search trees"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6644751"}},"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":"Q2829265$D29640E3-AC65-498A-ADFA-DE93D980E665","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d0b8ccbf8185e25465cb370eeeb0f0935615cc92","datavalue":{"value":{"text":"Automatic Functional Correctness Proofs for Functional Search Trees","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2829265$F261A4B7-A12D-41E4-8F51-04CCA371CAAC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9c9ad89ebcfa100fffc9a4309b28c9615ef4bf2d","datavalue":{"value":"1478.68065","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829265$7F15BBB1-742B-4590-894C-C43FFDBC1E0D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"84463d70e5fd90c2fff42af5ff552f78dcff60b8","datavalue":{"value":"10.1007/978-3-319-43144-4_19","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829265$83EA45AD-5889-40FF-894E-15F6A909E5C6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bd39997decddd4925a8ef09cbbffc4f41d2b1f00","datavalue":{"value":{"entity-type":"item","numeric-id":670700,"id":"Q670700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$7F225FCB-458A-4EC0-8405-7F603C492D73","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$B3183CE1-1C70-44E1-AF58-3DD4FC9B0B0A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3adf6ceedb6d880e3aaf819e51e828456bb3558d","datavalue":{"value":{"time":"+2016-10-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2829265$DE16F0E7-C3A2-48C7-AF64-FA0CB335F984","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829265$D19E10A5-9140-47B7-BC26-C911DBD2AE29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829265$AF764380-0147-4BB0-A9CB-3837D1F58A5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829265$4818D6B5-A4B3-4D4A-B03B-4C706A727644","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"33bd3882c7cddaede3d55ddf63f54db9daf38833","datavalue":{"value":"6644751","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829265$92EA31A9-FC39-4808-9F27-3CEE57E84598","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0dd9f12cfff5e16518b98dae67da0e7342fa8b7f","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$6134383D-3045-43CA-848F-73331A09BCFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d4a4b9328aeaa198621796249011494635ff553","datavalue":{"value":{"entity-type":"item","numeric-id":2551313,"id":"Q2551313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$7A0C27FD-5FF0-49DA-B0B3-F34ABDCD0679","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"11eefd7e7dc86c1755a8db4c6825e6e9fdeb6d39","datavalue":{"value":{"entity-type":"item","numeric-id":3619797,"id":"Q3619797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$2BEE3E2B-0282-4052-9B94-278E04B8C6F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98589d6fa667da17f782a55cd2dc8c33d4dbf671","datavalue":{"value":{"entity-type":"item","numeric-id":5308710,"id":"Q5308710"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$4FE74440-B7A5-4074-B0DF-D4F1D243C97B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da0d795517e293a55fbffeee6d84c637293c8bf8","datavalue":{"value":{"entity-type":"item","numeric-id":5327339,"id":"Q5327339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$617A379C-11EE-447D-9F83-0330544D3347","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2d4c5660dfe1c23de7141850de5bf4cfea3bf5c","datavalue":{"value":{"entity-type":"item","numeric-id":3648351,"id":"Q3648351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$9DD4DA32-585F-4534-8915-0811F1844545","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db463348657cf41d5ff4d422c54e0c686e6e5dfc","datavalue":{"value":{"entity-type":"item","numeric-id":2554952,"id":"Q2554952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$75BCC749-4F2F-4C52-99E0-ECFF40DB8CC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"972bc1fa971fc360b4e9b78570fbe5c71387879c","datavalue":{"value":{"entity-type":"item","numeric-id":3939197,"id":"Q3939197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$DB0D1227-CCE5-45E3-8E28-193AA9A5CE5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c5d8efd78c2ccca8211b4d28a521e2a96aa6af8","datavalue":{"value":{"entity-type":"item","numeric-id":2757083,"id":"Q2757083"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$DB3E96F7-D41E-4508-B9CC-1D79524CEA81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2187db9223a8d0a150779ea9f6a10844091469ac","datavalue":{"value":{"entity-type":"item","numeric-id":2850669,"id":"Q2850669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$638078BF-AEBA-4A2F-ADC6-F5074F7517F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"326acb68a6334a1c116e21985f2d11f27d8217d8","datavalue":{"value":{"entity-type":"item","numeric-id":4725724,"id":"Q4725724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$86B2892E-5EF3-4B95-B55B-05F80B3E8971","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"997214a7b55ffabdba512d09541bacb2e1bdf519","datavalue":{"value":{"entity-type":"item","numeric-id":2945642,"id":"Q2945642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$8B2EB308-ABE0-43A3-AB8A-6D93A9948083","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e264974062f53b439460b85662778a60b49509d","datavalue":{"value":{"entity-type":"item","numeric-id":2926333,"id":"Q2926333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$879DB8D6-E488-499C-8748-C571E9132F99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$41D29C8E-1885-425F-95A0-848FD0C44A71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"49a8d50e2ac3112c2b5beab9a321e48e86e40e67","datavalue":{"value":{"entity-type":"item","numeric-id":4702190,"id":"Q4702190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$F1D6D62A-9A55-4278-B71F-35388C74121C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"378c99ea6417f0d2e580a3615c9fde65e65561ae","datavalue":{"value":{"entity-type":"item","numeric-id":4096430,"id":"Q4096430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$C51E18DE-536A-4252-9F41-7B2A7B94B0E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aab32d3508a26f5a5ad4fef940ce6677a9f5992e","datavalue":{"value":{"entity-type":"item","numeric-id":3875357,"id":"Q3875357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$465C5DCF-C14F-4E6F-BE62-7AE7FACF8BFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e00db80b77d8200c404d1a2e8fc24d94da053bc","datavalue":{"value":{"entity-type":"item","numeric-id":1193748,"id":"Q1193748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$F36D500A-DC74-481D-89D9-FBD98065CE5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0f53d9231bc5ff64922d7dd218bb49071786117","datavalue":{"value":{"entity-type":"item","numeric-id":3768416,"id":"Q3768416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$5543FF25-4872-475B-9E27-3BEBA078C8F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1fc17e4dbbbc6e7870b651c8c92e52bfaa3d84c7","datavalue":{"value":{"entity-type":"item","numeric-id":4864245,"id":"Q4864245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$11AB499D-1379-4793-8B56-95A944C2FA9F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$6891A63C-278D-4D14-9866-E8D324EBF964","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$1B6C4552-F5A4-4760-8B37-773AFEFAFC66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$E2A672D1-CC12-4651-BEA3-7EC9CF7549C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$C38D3FCD-F957-4D15-B5B5-E5071DB5CD70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e338912f65cbd77347bbd512933e55736ef58bd1","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$031E59D7-48D3-4A91-AD5C-C91DB4580DAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"12d56fa0ed9e831c57bfb8cee200e30f869b2822","datavalue":{"value":{"entity-type":"item","numeric-id":40288,"id":"Q40288"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$B677CCDF-2347-425F-BC44-410024DF01F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"23371b1f220fc300d91247f371d0002330f9322c","datavalue":{"value":{"entity-type":"item","numeric-id":40242,"id":"Q40242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$67B086BA-29BF-4EA8-9ACF-FCE95A749886","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0b1eb0401b7aa76d1b64b4825659dfb31c923265","datavalue":{"value":{"entity-type":"item","numeric-id":40320,"id":"Q40320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2829265$5B5EA3AE-986B-407F-A213-AE9394BC79BB","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":"Q2829265$10500CAF-6B79-426A-9393-BABF238FC6F7","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1838d6e5511d616c06f2fc8909609ac9ed6961f7","datavalue":{"value":"https://doi.org/10.1007/978-3-319-43144-4_19","type":"string"},"datatype":"url"},"type":"statement","id":"Q2829265$7CF09E4F-E3BB-4F62-8A68-266041980008","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0e11606d67ac76e40ed897baa0309690dd56df5b","datavalue":{"value":"W2483569599","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2829265$A4F34CEE-1110-4600-BF65-E0E98C91A780","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"40fc5e7043528b48f48513ad3d7973b2a19e7a49","datavalue":{"value":{"entity-type":"item","numeric-id":5056001,"id":"Q5056001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5cd2c85bc3620f86e908837e94c3284b272903c0","datavalue":{"value":{"amount":"+0.7960885167121887","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":"Q2829265$08791DF0-8C69-4E36-8FD6-ED665AEA0F9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13ca106ca069b7bde1da5e78d2bd00fc47c44ee5","datavalue":{"value":{"entity-type":"item","numeric-id":3648351,"id":"Q3648351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9001848bdb78f70b98e6a1d38dfb6d5729405722","datavalue":{"value":{"amount":"+0.7528698444366455","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":"Q2829265$72EB326D-561E-4EAC-995F-0F84E45254EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4c6b35387f99eed794998dc4dbc6f1b99c1ec2e0","datavalue":{"value":{"entity-type":"item","numeric-id":4943361,"id":"Q4943361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"99ec97fb959357720291e4a04c5bf14d44acd55b","datavalue":{"value":{"amount":"+0.751259446144104","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":"Q2829265$54DDE35A-5CC9-4270-B159-CCD93E685F26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"24ad6160359367d315465542a8055f597ea93122","datavalue":{"value":{"entity-type":"item","numeric-id":2942864,"id":"Q2942864"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a9b7a92dae0197ffc746cc9f3219d23ca160a51b","datavalue":{"value":{"amount":"+0.7497401237487793","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":"Q2829265$155F45A4-4A74-4917-AAC5-7FCB175D285B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85d2ea3cd98365ad96a31aff0fee17031404a04e","datavalue":{"value":{"entity-type":"item","numeric-id":5434520,"id":"Q5434520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f5f41a02df75b1d8462dfdc7915311c811249863","datavalue":{"value":{"amount":"+0.7437559366226196","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":"Q2829265$E94225F5-6101-4A87-9791-99FA7B4F01DF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2829265","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2829265"}}}}}