{"entities":{"Q5741556":{"pageid":7771107,"ns":120,"title":"Item:Q5741556","lastrevid":92865101,"modified":"2026-06-05T02:57:18Z","type":"item","id":"Q5741556","labels":{"en":{"language":"en","value":"Partiality and recursion in interactive theorem provers -- an overview"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6607272"}},"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":"Q5741556$2FC53DFC-3BA8-46D3-A6EE-AD1A253C6873","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"46e6e33addaf569f188d6ebc8378fb756f251d5c","datavalue":{"value":{"text":"Partiality and recursion in interactive theorem provers \u2013 an overview","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5741556$0EBD6A7C-B236-474C-9336-7DFD5A11FDC0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0d0cb9eff3f7f28906fde259e423ef176c8fd802","datavalue":{"value":"1361.68186","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5741556$CA690981-8A91-4620-8BC8-858CE401FA2B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"94ce9596de9961f62a7d5c2601de657897996268","datavalue":{"value":"10.1017/S0960129514000115","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5741556$2517A1BD-43B5-4EC9-9A84-BE3B70765988","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"43fa8ed1a432c4af2ca647b623e8e3f5c6fe6565","datavalue":{"value":{"entity-type":"item","numeric-id":1744409,"id":"Q1744409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$10BD671D-F53E-4E02-A9D3-3C83AEA72D1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bb9a75665101462bc01a2c7426c95f31a74ce050","datavalue":{"value":{"entity-type":"item","numeric-id":438557,"id":"Q438557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$C1B5F82F-8491-45EA-9676-B23FAFF77933","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a9414558f268ee594724569b856f23c96f190f01","datavalue":{"value":{"entity-type":"item","numeric-id":1791139,"id":"Q1791139"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$F6E7F105-7F26-4703-9252-1AB658FB59C9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a53527e88e2413966f3c8ce14c92b878c452756d","datavalue":{"value":{"entity-type":"item","numeric-id":2709784,"id":"Q2709784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$09EC0B30-D93A-428C-8A4B-7027FFB8BA53","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"983499d539ab43bbb6f5e5531bc62eb931d87235","datavalue":{"value":{"time":"+2016-07-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5741556$8367C864-C43D-44BD-9D64-853DB4EB4015","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5741556$53602007-EB65-462C-847F-E86F7B4325BB","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"085abca8375cdde8592e8b152325bbcb803747f4","datavalue":{"value":"6607272","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5741556$47DC74F3-34F9-4E6D-AE7E-6260DE3DC783","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"067e00213990a6f2431e78667be3f10443c92f4f","datavalue":{"value":{"entity-type":"item","numeric-id":16052,"id":"Q16052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$EEBDDFBC-8B76-473F-835C-9B43E8BC6F05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$BA456FEA-294F-429B-9D51-A1499FDE5D09","rank":"normal"},{"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":"Q5741556$518DE312-7736-4BE6-B784-062ACA7D6F1A","rank":"normal"},{"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":"Q5741556$DDD88949-4DBD-498A-86C7-289B00BDF7A4","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":"Q5741556$7E100654-772B-4562-8354-84893EDB1E87","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1972f4e4751e04e48bdf5bc3b5cc998d4b554b26","datavalue":{"value":{"entity-type":"item","numeric-id":2892763,"id":"Q2892763"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$80576833-6A48-4CD0-8611-47733ECC5F50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"351df2a8b1173f3d3a83aebab494a1f900b8f514","datavalue":{"value":{"entity-type":"item","numeric-id":1029815,"id":"Q1029815"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$A287D24B-DB19-4281-9268-04D6ACEA33FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0750119319825b48163ea7e9aaeedc16167046c","datavalue":{"value":{"entity-type":"item","numeric-id":3612623,"id":"Q3612623"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$65154947-FD9B-4ECD-A01F-972840B25DCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b7fccd560221ea7f03064eaf67187aa99c6ef8f","datavalue":{"value":{"entity-type":"item","numeric-id":5697711,"id":"Q5697711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$0C9F515B-CA9E-45AD-B9AD-4EDE37FD8B67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ab5d7b35f67f940445411fa45c1b02bcb40d39f","datavalue":{"value":{"entity-type":"item","numeric-id":3999860,"id":"Q3999860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$B572DF11-5CB6-4F50-BDA2-CDD62139B7DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1420eb5b183c580e3eaa2025b4097787d860ff45","datavalue":{"value":{"entity-type":"item","numeric-id":1112584,"id":"Q1112584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$27DF18D3-D938-4699-B160-E0A000D18ABA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"923d9841ebb82ba7564626f46c70dd17455ed552","datavalue":{"value":{"entity-type":"item","numeric-id":4267723,"id":"Q4267723"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$F52C1E85-001A-4240-82AC-246AFF2A1259","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":"Q5741556$30536AF2-DD06-4478-87D7-2AE24DE31438","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df8c2eecaa019d2eaa208d6ac51a516597ddb9b6","datavalue":{"value":{"entity-type":"item","numeric-id":757075,"id":"Q757075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$BCAF380C-AD45-4CE7-A873-D528715F11E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3893e24895c818d766b4ac601e2292c1956a8e2a","datavalue":{"value":{"entity-type":"item","numeric-id":4819653,"id":"Q4819653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$E4B495F5-F9A3-418D-828C-D70A79532ECC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ce4c2361ad25be1e2dbfc97b6b7c482747c81ff","datavalue":{"value":{"entity-type":"item","numeric-id":5191089,"id":"Q5191089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$1941FD4C-CC7C-4A94-8931-0E7DA39D1A4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22e678cfddf453ace95d62268a3ca88ca789ec4a","datavalue":{"value":{"entity-type":"item","numeric-id":3160301,"id":"Q3160301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$428EFDE2-4E1A-4D77-8DBB-6E9B7D5C8154","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f7396a7d7693b676318207b9fce821ae1fe747e9","datavalue":{"value":{"entity-type":"item","numeric-id":1425160,"id":"Q1425160"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$B2843602-110B-406F-9C09-1F00C19A5351","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16c58bccac3eb8e167d77acc1c92ca853e7a5fcc","datavalue":{"value":{"entity-type":"item","numeric-id":2655326,"id":"Q2655326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$438C6C56-B234-4EE5-B2E9-544AE1EED3B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f7aefe830c417bbf0aaa4cb5862ce28580e41e47","datavalue":{"value":{"entity-type":"item","numeric-id":3540199,"id":"Q3540199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$FBFD491D-3754-4D83-9082-9F8923A9A8D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14b77c50b47b4c19657d295ea46a35a19d800721","datavalue":{"value":{"entity-type":"item","numeric-id":5387897,"id":"Q5387897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$24F85CFA-6CC1-4E5F-942F-0A1DFA1DCCA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26dac06384dc787a405949068340510a6602af80","datavalue":{"value":{"entity-type":"item","numeric-id":4463991,"id":"Q4463991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$3D0F7723-87AC-49DB-9172-C7A3BFA1AA85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad38e0ef5109c872fd15da36ed5bb76b94d70ec6","datavalue":{"value":{"entity-type":"item","numeric-id":3434629,"id":"Q3434629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$0A5DD78C-218E-46AD-9635-96CC49C35C0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f474b409a8f3415f67c4fa840940f857e860d83","datavalue":{"value":{"entity-type":"item","numeric-id":790610,"id":"Q790610"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$EA94193B-8B9A-4053-83A8-1F9539439678","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"470336b86f7e93b9af304caca1999cfc5d661f50","datavalue":{"value":{"entity-type":"item","numeric-id":4130959,"id":"Q4130959"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$34CE0F32-E011-4228-B741-3067E492FEE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78668ae87248f7a1c29024ec1dc4abe60aff1595","datavalue":{"value":{"entity-type":"item","numeric-id":3559770,"id":"Q3559770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$FEDF00C3-3EAC-4A65-8B06-5FACBF5D7AC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f0278a622341c2c3ea684f66af68a5b07b0b894","datavalue":{"value":{"entity-type":"item","numeric-id":972425,"id":"Q972425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$0641F954-74DB-4B58-B23D-58A62413914B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f8a0484d56d68801f0437288a1ce7994f7539d9","datavalue":{"value":{"entity-type":"item","numeric-id":3608789,"id":"Q3608789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$BA94FB5E-8A71-4531-B0ED-C89CCCF248BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a98e1d68003b0040c15c163e66f3fd9578fb9386","datavalue":{"value":{"entity-type":"item","numeric-id":3997074,"id":"Q3997074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$03F450B8-7FBA-49AB-AA08-05B6329FD8B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5043892a0e511359188ed62fdaa6bd089f0b3629","datavalue":{"value":{"entity-type":"item","numeric-id":1314363,"id":"Q1314363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$2EA808D3-F4EE-4052-AD91-E8FC419ED4BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f08d6a93b5519fe40946b3c81233b0a486a55307","datavalue":{"value":{"entity-type":"item","numeric-id":4414308,"id":"Q4414308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$A0F62A72-7B7A-4D18-8963-94021214074C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1404903fbb3450c69ae4b46e148487834232fe43","datavalue":{"value":{"entity-type":"item","numeric-id":1823013,"id":"Q1823013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$EC9353D1-5CE9-4B8A-99A0-3322E7104FF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8f88db4db4ff3067bd759c8807bea327b3eccfd","datavalue":{"value":{"entity-type":"item","numeric-id":1094421,"id":"Q1094421"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$8463DF7A-AE88-4552-BE9C-7AAAC312790A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1963c91159758135960a0efef55c7dc5fae818e4","datavalue":{"value":{"entity-type":"item","numeric-id":3183534,"id":"Q3183534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$8DD1689D-62E0-47B2-A916-F72514494FDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"931c42c28f22f89fe1b66164f9ececc2021ac1a2","datavalue":{"value":{"entity-type":"item","numeric-id":3558332,"id":"Q3558332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$51181A7A-175A-4E80-9B47-0CE06CF0A370","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$1650099E-FEB2-489D-A11F-7A9158172607","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"97aac3e9983bb038948e2fba3a98c71cc7d8d801","datavalue":{"value":{"entity-type":"item","numeric-id":5757920,"id":"Q5757920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$0752D40B-B971-422C-A6F3-5DF4739A0BC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c38bf30473891f925b8eae2804f1a04e3e3de28","datavalue":{"value":{"entity-type":"item","numeric-id":1595923,"id":"Q1595923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$855D27C2-8095-47FE-879A-5E2BEE56DDEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c02ff547cfaf7e165513cf8f07ad1a1e28baa67e","datavalue":{"value":{"entity-type":"item","numeric-id":1367078,"id":"Q1367078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$E23B5758-1C74-4072-9281-31C04ACD6D0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b05f5e5a6c7354caaa9141196fc1e92ff4579eb6","datavalue":{"value":{"entity-type":"item","numeric-id":679251,"id":"Q679251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$EAC0CF9A-5857-4B95-820C-2745B70D68D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e2dade93a965b4ec7651716b5bb52a35509088a","datavalue":{"value":{"entity-type":"item","numeric-id":1314643,"id":"Q1314643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$0E67A34B-3166-46A9-9660-B1917C15ACDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"364525b70d80e5ad032dd4bcb752b39f36195669","datavalue":{"value":{"entity-type":"item","numeric-id":4508246,"id":"Q4508246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$F663FDE6-7445-456B-B759-164B7F9E5C7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$9E31DB99-82E0-4FDD-89EE-BD9BAC0A17C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d7aea7368304c81d99f05a85147c94cac452455e","datavalue":{"value":{"entity-type":"item","numeric-id":3523164,"id":"Q3523164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5741556$EAD928EC-458A-4775-8342-20818B3677A2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"730fe866201adda4dc6cd9d1e7f780278b487d5e","datavalue":{"value":"https://doi.org/10.1017/s0960129514000115","type":"string"},"datatype":"url"},"type":"statement","id":"Q5741556$61651A47-2102-4294-A116-EFD331CC9B43","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0da19b9f0a8cb7222d5e0b9fe138ea5f5ea3023d","datavalue":{"value":"W2023353691","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5741556$72A3147D-4D23-4C18-A31D-C19A03B80276","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8119ec3aa981e9a9db002ac60c0b87fa899679f0","datavalue":{"value":{"entity-type":"item","numeric-id":679251,"id":"Q679251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"007185aa9e7e0990ccbe2d32919f66ac01e2cf8e","datavalue":{"value":{"amount":"+0.7811526656150818","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":"Q5741556$A55CE24F-6AF8-4760-A931-064DEEF3D607","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"63392152ceac32be176b948e503f3e589a506710","datavalue":{"value":{"entity-type":"item","numeric-id":972425,"id":"Q972425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7be65ee1244bea9d7b94bb5b5328a88c8058bbb6","datavalue":{"value":{"amount":"+0.7800580859184265","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":"Q5741556$689C0009-77A7-4E01-9E59-6D5E33DA945F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb33dbf764138f812d35e37589bcb282274e2082","datavalue":{"value":{"entity-type":"item","numeric-id":3613436,"id":"Q3613436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"99cd976392b9e9337da532410e74da04a2c8eb2a","datavalue":{"value":{"amount":"+0.7700137495994568","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":"Q5741556$9729F01B-C0B5-4DC3-8169-9CCCF1090EEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13f12cc42a11f603ff3a7078a8ce829374450f4f","datavalue":{"value":{"entity-type":"item","numeric-id":4790656,"id":"Q4790656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5d9f1304bd103f9772a45cc4f73038844087e524","datavalue":{"value":{"amount":"+0.7612144351005554","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":"Q5741556$0071F1C9-AE47-43CC-9B7B-15A52D7B33D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"704a49cab08e72b5b7eb95f34ca27569ea97ba64","datavalue":{"value":{"entity-type":"item","numeric-id":1595923,"id":"Q1595923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"000fff8f3762192ee6158768c60da076d8f49f7f","datavalue":{"value":{"amount":"+0.7509362101554871","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":"Q5741556$6AA7ED3F-85E6-4262-AAD1-48F496F62756","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Partiality and recursion in interactive theorem provers -- an overview","badges":[]}}}}}