{"entities":{"Q485837":{"pageid":487604,"ns":120,"title":"Item:Q485837","lastrevid":62256795,"modified":"2026-04-11T04:51:14Z","type":"item","id":"Q485837","labels":{"en":{"language":"en","value":"Synthesis of list algorithms by mechanical proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6386140"}},"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":"Q485837$805CDBFB-47EC-4F0C-83B5-50170FC671D7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"785fadd6463d23ea57ee09453ec49490e2fb3590","datavalue":{"value":{"text":"Synthesis of list algorithms by mechanical proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q485837$5C2078A3-CB2E-47D2-A72B-3F06476F0E00","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3446b65a2a40f7624764741c0c49fdd4fe3c048c","datavalue":{"value":"1315.68263","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485837$3ECDE659-3DA3-4FCC-A0C1-0CB283CDFD80","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b2334913bd300f77e4121ff8b958800142e55ceb","datavalue":{"value":{"entity-type":"item","numeric-id":485835,"id":"Q485835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$ADBC1E19-A399-47E9-85C0-0C0BBB7E86D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"725aca679a0cd849b7123b8f0d65ff45506c8d40","datavalue":{"value":{"entity-type":"item","numeric-id":485836,"id":"Q485836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$93BB0977-270A-4A09-8B6C-3FE4741CFA7E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$96A42CFE-B986-4864-A392-A77AA459CB6F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"263261338df616964a138c38a6f0c5b7f36f1f12","datavalue":{"value":{"time":"+2015-01-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q485837$3F0EC6A0-9790-42E7-8860-EBC20CFED97E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"1bcdc2a107fd2414d151e8610f3471a8784e75bf","datavalue":{"value":"68W01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485837$D4C94188-9BE6-4E30-AC66-F9E903263B20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485837$D85A1ABC-64EA-48AA-A1D9-1D698CBE94FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3f97694d44af155a68434cb72eabc6a4d5dd5227","datavalue":{"value":"68P10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485837$142D23DF-F160-45A2-AEB4-5D49812C7270","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485837$646BAEF2-B86A-402A-BCAD-41C708300BEC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cd0d629fb7d71c3f722003d2f8b3e111720c0724","datavalue":{"value":"6386140","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485837$84D26EF3-6105-41FA-B1DD-7386626E6E07","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8966b62df322b0dd54865da77149f7978488b880","datavalue":{"value":"list","type":"string"},"datatype":"string"},"type":"statement","id":"Q485837$4A7D24E1-DB9A-4F69-AB87-0E619DA0D304","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc8be07ac551ab83e4335385a09ae0b05d11975d","datavalue":{"value":"algorithm synthesis","type":"string"},"datatype":"string"},"type":"statement","id":"Q485837$C79AF715-4BAD-4BDB-9D6A-D2141D9716FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"37db48fc50878deb5298f058e27a669b8c15ab38","datavalue":{"value":"Theorema","type":"string"},"datatype":"string"},"type":"statement","id":"Q485837$8419C009-59EC-414D-B94A-CE8F4C53D5B3","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d89eed7087f93c1cdf4120c868b02779d34eaa8b","datavalue":{"value":{"entity-type":"item","numeric-id":13309,"id":"Q13309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$BF0E3D4C-0B98-45F9-94C1-E9913095D925","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"261ae6dfeffd96c9ea238e124055221c78337064","datavalue":{"value":{"entity-type":"item","numeric-id":13705,"id":"Q13705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$D21125B5-DC0C-4693-BA35-B1036B330762","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":"Q485837$B333E4FB-747A-4A25-A731-1F08F82178AC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b3d97f9a4b252b9ead0b53fa630fe8c0ee4c2b67","datavalue":{"value":"https://doi.org/10.1016/j.jsc.2014.09.030","type":"string"},"datatype":"url"},"type":"statement","id":"Q485837$E6C60892-9F6C-4346-A658-B24D928C693C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3ff6db623ff1e60b9958d951e96525c4ac3ae6c5","datavalue":{"value":"W1988598795","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485837$8E4F5090-90C7-49D2-B7B2-9BC8B9D134B8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"42df289460c4776200519dd71f2cab731f946aec","datavalue":{"value":{"entity-type":"item","numeric-id":1259168,"id":"Q1259168"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$FCF944A5-7FD4-4DB9-8B8C-D7D3D296C295","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"53ee1ce1792d692329898f0a992aeaf81279eee3","datavalue":{"value":{"entity-type":"item","numeric-id":5712543,"id":"Q5712543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$15D32E1D-AF76-4753-8923-008B34133904","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cd705a1c4c13e7602f282c4e64be62fd689b41c","datavalue":{"value":{"entity-type":"item","numeric-id":3219093,"id":"Q3219093"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$D57249DF-760C-4246-9EE3-1091F813F2F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65627a8a26bdf026d150a63c4a81347aa5a9f9bf","datavalue":{"value":{"entity-type":"item","numeric-id":5699466,"id":"Q5699466"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$F4FCD57E-5773-4076-BDFC-8CB4836FAC25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec9faf009dcc84ce1efe32f21621c535b7220fd1","datavalue":{"value":{"entity-type":"item","numeric-id":2847391,"id":"Q2847391"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$CF0B2125-6861-425E-9AFC-FD899095F178","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1616035475940e78f5e7ffe6b447afdd22db3a38","datavalue":{"value":{"entity-type":"item","numeric-id":3416408,"id":"Q3416408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$18FC17BA-DED9-48E3-815F-D65B4E566521","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c7e013849775846918727fac3e7e6455bd448813","datavalue":{"value":{"entity-type":"item","numeric-id":865646,"id":"Q865646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$C8470F7A-E8C5-477D-A5CB-614ECC639A9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b66ec052635085a611a72ee91433db7ef7a5fa2a","datavalue":{"value":{"entity-type":"item","numeric-id":2751543,"id":"Q2751543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$A8F732DD-326C-46D8-88DF-E4D0BCAACB90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"661364c39b0d1ca298a77bc970439cd4e9a0507b","datavalue":{"value":{"entity-type":"item","numeric-id":4226993,"id":"Q4226993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$994D2E44-F89E-4E14-B3E6-D74327AD8138","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0a42635e354ed5a90dff7abb6b01b6c7ff160dc","datavalue":{"value":{"entity-type":"item","numeric-id":5462949,"id":"Q5462949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$6F697340-9607-4475-A6FF-8D99E642730F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab8ea372caa817f188e4e943a4cbc2ab55cc9d12","datavalue":{"value":{"entity-type":"item","numeric-id":5549412,"id":"Q5549412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$B57C7093-0686-4D54-A031-E0198D375EC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d346d8485da0bc889f787fa277d331b616d4df2","datavalue":{"value":{"entity-type":"item","numeric-id":4054648,"id":"Q4054648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$4D90FF69-CBDD-426D-952C-AB0CC0604596","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a855faf9fd36b10ff39c0860ddc943b205994344","datavalue":{"value":{"entity-type":"item","numeric-id":3862422,"id":"Q3862422"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$C9688D50-E914-40D2-A138-71EFF8E79E5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"02be31bbcccdd5668a4bf38db4eb874de330c10d","datavalue":{"value":{"entity-type":"item","numeric-id":1051424,"id":"Q1051424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$CD3FB3BE-07B3-46F5-8E41-78286FE174B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05a8530cc8341477c91a6a458d8bc3eaffcd6c6d","datavalue":{"value":{"entity-type":"item","numeric-id":1251072,"id":"Q1251072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$BC7B36F7-3C9D-49C4-9B2F-A9A793EB40BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"afa2e78b2c8f62bc01c953d0d9ef301476ca64fa","datavalue":{"value":{"entity-type":"item","numeric-id":4305630,"id":"Q4305630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$6D74413D-CE54-4BF4-83D4-836CE9BB1FB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d41d71a0adbde6caf00b749ad37ee0e9ec473936","datavalue":{"value":{"entity-type":"item","numeric-id":4707743,"id":"Q4707743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$3EDC7D34-33E3-47C2-9407-6E0F07445EFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2dbf5d4c6cedd5848e03816494729378cde53a8e","datavalue":{"value":{"entity-type":"item","numeric-id":2551698,"id":"Q2551698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$6198B87C-263C-4848-A209-B3364FD98BCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1fe67b65727389c17ae1cf9ee01424d6547a522d","datavalue":{"value":{"entity-type":"item","numeric-id":1915136,"id":"Q1915136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$2F0AFFC2-56D7-4098-885E-5AD43AC16E98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2d8a82c54657d02bb198ddd93f92ea9107dc67b","datavalue":{"value":{"entity-type":"item","numeric-id":5313058,"id":"Q5313058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$E330CEFA-F514-47A4-994B-9F432C0E064F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0e4d32e6c7d60e17d4c223d66d4caf8bac165b1","datavalue":{"value":{"entity-type":"item","numeric-id":1118415,"id":"Q1118415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$68B9A1D3-8F1C-4DE7-8FED-8FA8B574CD6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b26b52e432dbd456c2997e91926441e72642f519","datavalue":{"value":{"entity-type":"item","numeric-id":3206282,"id":"Q3206282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$57EC2ABD-2AEE-4ECC-9389-57D9D84082B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"44d5e3e8e4f94b1b6bb64dfc894b1e98e8ca85db","datavalue":{"value":{"entity-type":"item","numeric-id":760206,"id":"Q760206"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$28F629AF-298E-4AF4-ABDB-E8DD9EC0D34E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c77dc933c73e4695de7ff6375817b86b37737aa","datavalue":{"value":{"entity-type":"item","numeric-id":3922132,"id":"Q3922132"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q485837$91365131-A419-4DB2-BA9A-F2D1FFD76BC7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c3027e772cd6f05b334ea0293bb7d9e5e46316fd","datavalue":{"value":"10.1016/J.JSC.2014.09.030","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q485837$A274FB43-F964-4186-878A-948686972CA8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f4573333321c1089120c550486de7c0d46a23e54","datavalue":{"value":{"entity-type":"item","numeric-id":2798749,"id":"Q2798749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a5a427d93b0610fab103ee586baf80f80304bc6","datavalue":{"value":{"amount":"+0.8552145957946777","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":"Q485837$64BE10F9-911D-483F-8F6D-7E2E780B8B39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cde683b9c56c8a29a5e3986c12bfc7e68c0b8413","datavalue":{"value":{"entity-type":"item","numeric-id":1996870,"id":"Q1996870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5704a6d1a12bcc0a800ac79353b5aefe52803e6f","datavalue":{"value":{"amount":"+0.8501177430152893","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":"Q485837$667D3221-8824-4BFC-AB40-BC5FAB83488C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2df768e7a5792925da6d68bd86c52ae05c8f11d8","datavalue":{"value":{"entity-type":"item","numeric-id":1640636,"id":"Q1640636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"acad210b6f5307683293c68dd1f4c943a08fc683","datavalue":{"value":{"amount":"+0.8291293382644653","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":"Q485837$6175055F-B56C-4B3D-BAB4-068A3AD00D3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"26377171112486b33026ddc7b78658a0583ca1b0","datavalue":{"value":{"entity-type":"item","numeric-id":1822927,"id":"Q1822927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"55b8ce09dcb7b6ffde942a3b1403bd5df44d77e5","datavalue":{"value":{"amount":"+0.801798403263092","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":"Q485837$97CF8CBC-8746-40CC-90CF-6AEF7B38B7A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b2ef1dfb8450e1a64b77276d877120e7c94cd7d","datavalue":{"value":{"entity-type":"item","numeric-id":4023948,"id":"Q4023948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b584d9dee7a93360587ad6a9a8a5c50a82d5092","datavalue":{"value":{"amount":"+0.7700146436691284","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":"Q485837$6DA6B2FE-5D52-4C8C-9BF7-070CB6390498","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Synthesis of list algorithms by mechanical proving","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Synthesis_of_list_algorithms_by_mechanical_proving"}}}}}