{"entities":{"Q2175214":{"pageid":2185957,"ns":120,"title":"Item:Q2175214","lastrevid":78271004,"modified":"2026-05-06T11:11:52Z","type":"item","id":"Q2175214","labels":{"en":{"language":"en","value":"CryptHOL: game-based proofs in higher-order logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7194394"}},"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":"Q2175214$4EF10C76-DAEB-4277-A3C7-760FCFF06B34","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"142c9715e26375d8dd935cf7d54f1369496433dc","datavalue":{"value":{"text":"CryptHOL: game-based proofs in higher-order logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2175214$43F3E253-8656-460C-B63D-73FC9632FC67","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e80a21c12af2f67f4d1ddc30765a2ee762f0eb9f","datavalue":{"value":"1455.94121","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2175214$71236E4D-55DC-4C37-9725-8297D5C58F60","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b18da065d50ce37e447f1f6708524421ab8f031f","datavalue":{"value":{"entity-type":"item","numeric-id":1663232,"id":"Q1663232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$9611F01A-D06E-4600-8039-16452004560C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"923e87eee3cccd3fc47dfef51662370c7d5088f0","datavalue":{"value":{"entity-type":"item","numeric-id":1722646,"id":"Q1722646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$F0580DFF-D79E-4B8A-9196-7A52543F6049","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"69ad79c07c2956f1777e7c914202daf6884a50fe","datavalue":{"value":{"entity-type":"item","numeric-id":1332774,"id":"Q1332774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$2E04FF44-32C3-4B91-A17A-4DA408B2018A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d5eab3bbb3b6673353b9ed770934b15d004ef795","datavalue":{"value":{"entity-type":"item","numeric-id":166358,"id":"Q166358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$A38C76F2-E312-4650-B121-610D8D36C93D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"55f830d516df43c194c0b51361c606f2f40fb25b","datavalue":{"value":{"time":"+2020-04-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":"Q2175214$82AE27AA-D6DB-4EA4-AE1C-7F9370E96BCF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b3f5570531d36cdad95fcc8cba24a2dabc5fbbbf","datavalue":{"value":"94A60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2175214$72C38CAE-05DC-4048-AC82-87441C48F926","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b71b42e4e887bf125b7436fe1334aef39047fb5c","datavalue":{"value":"94A62","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2175214$203C7D49-1797-43AA-A94C-BF9785C9D4F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2175214$C1A33D39-83BF-4B06-A790-CEBBBCEF70EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4782ec55a8b8cc3ebd55f173b4568991ce0fd6ad","datavalue":{"value":"91A99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2175214$0FCFDF45-FC09-4E16-984C-81E10ABBED8D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"49c12e0006f95db3839b806d2b368caf766e584d","datavalue":{"value":"7194394","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2175214$54ACECDF-B18D-4EC7-B8E5-BF394D222120","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"564664e04ed8722ea9a8797361f6b33443e431ed","datavalue":{"value":"provable security","type":"string"},"datatype":"string"},"type":"statement","id":"Q2175214$867B8287-1786-423A-982E-7774BAFC2998","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1bbdb92223329e4e45ee35367f649353e78c5138","datavalue":{"value":"game-based proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q2175214$6EEF94AF-1D9B-4082-8F4A-BE6E80189313","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2175214$A1D7C62A-4FAB-4A53-A4EF-8A1DD4BB8974","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2175214$D9D6B1E8-C77B-4ACC-AB08-7BF9CC0D05FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q2175214$41149A78-9D6E-4C0A-A5B2-BD803BB4D450","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"8ee6d85615af38f49331175b703780973164d8fc","datavalue":{"value":"Q113906162","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2175214$253B4C7A-13CB-4DB6-A867-C580B6DEC84A","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":"Q2175214$B49E101B-C293-435F-BEEF-48505A7FA526","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7b8bfcbbb8584ed9cd8fa8ae699d0634f4084a68","datavalue":{"value":{"entity-type":"item","numeric-id":21717,"id":"Q21717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$74F44501-C29E-47F3-A198-4BF84D456365","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ae4173d13b960594f2bf5bfd22402fc0202f2b76","datavalue":{"value":{"entity-type":"item","numeric-id":40255,"id":"Q40255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$30F76FDC-819E-4ED7-BABB-B9851E09EFEB","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":"Q2175214$33AC2A92-4745-4907-B6F0-7B3661F35584","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d4d6d537e8cec84a5df24cd1f83bf781fd595341","datavalue":{"value":{"entity-type":"item","numeric-id":53713,"id":"Q53713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$BD63914E-79EF-4E6F-B2D6-A9B698572BD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"456283a32294a54ddde0e5f61990468a36608180","datavalue":{"value":{"entity-type":"item","numeric-id":53714,"id":"Q53714"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$03F7CC29-E745-451B-A515-7DEABC92892C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"085f0460b6b7c875415ceed9b026722ccb7b77d7","datavalue":{"value":{"entity-type":"item","numeric-id":53715,"id":"Q53715"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$FCE50883-526D-4F83-802E-C18112CBF919","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$933EAA2E-7899-48C8-A57F-2352160D10BB","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":"Q2175214$DE247E8D-8761-4F38-8173-FAB7A327AAA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c16bcc2a523bb7e68436e2f13725598b97d9a7f1","datavalue":{"value":{"entity-type":"item","numeric-id":32994,"id":"Q32994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$2BBCF041-DE33-4A53-84E4-693965898239","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$A4F86572-1DCF-4D99-BB60-BD8D7AE87F27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ed664df4807a1c1480dbcce90c73c0ac4e6b59b6","datavalue":{"value":{"entity-type":"item","numeric-id":24733,"id":"Q24733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$2EE0DBFE-7EC0-444E-948E-E2897778A817","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4e22b8176489c2409392314db08f466f9ad9c934","datavalue":{"value":{"entity-type":"item","numeric-id":30463,"id":"Q30463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$49A714E2-274D-4A0A-B02A-03D1D2A67CBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1f427ab6dbbd025b0c0b66dd047be36c332e9e80","datavalue":{"value":{"entity-type":"item","numeric-id":32822,"id":"Q32822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$D18EF316-404F-44B2-BAD1-06AAE39CFB8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e9fd7dbff509abaee9c64d21afb19f85055bad01","datavalue":{"value":{"entity-type":"item","numeric-id":32823,"id":"Q32823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$9877FD46-E763-40E2-AFB6-9DE816164763","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"17b6bf936b27bf52d41c01b7a092635fe801ec6c","datavalue":{"value":{"entity-type":"item","numeric-id":39279,"id":"Q39279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$97EC6F0B-7571-4CE1-A512-2F8BE98F4CFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"98535d36815e9957949f203b467e115b0c562b2b","datavalue":{"value":{"entity-type":"item","numeric-id":40296,"id":"Q40296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$DA2742F7-B04F-42A9-B42B-F9D5327659F1","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":"Q2175214$D3802B67-C26A-49BB-A700-5593A38EB872","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7626cf773f8703d15e785c926ad7c1d63ea38b6b","datavalue":{"value":"https://doi.org/10.1007/s00145-019-09341-z","type":"string"},"datatype":"url"},"type":"statement","id":"Q2175214$8BDC2B0C-93BF-4D90-8F79-BE7160FB67BB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"01237578fd67a0e4e64415a6296f6639cda0e433","datavalue":{"value":"W2751465014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2175214$372B24B3-3E06-4494-BAF7-8E83BC1FB553","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ccdafbc15f8115761e3b30cbc0ca4a6f9af9ef50","datavalue":{"value":{"entity-type":"item","numeric-id":5261630,"id":"Q5261630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$9D3BF370-BCF4-4AE5-9EE3-EEA41C89513F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1370d4ef41cfc490a43b42eec581952d43ac681","datavalue":{"value":{"entity-type":"item","numeric-id":923886,"id":"Q923886"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$A8656A2E-3F16-4611-BA53-DC8A878D9715","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5f8bfaa468e637db4889a8ff43ea6b011ceb641","datavalue":{"value":{"entity-type":"item","numeric-id":5505567,"id":"Q5505567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$03EA4227-802A-4EB7-831D-B2757BC2C2E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a83681413983b5c1cd346b7aeccc929ffc09104","datavalue":{"value":{"entity-type":"item","numeric-id":5408416,"id":"Q5408416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$24DCCB73-8437-4584-9D0D-B06A68E56F68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fd4c931786d4fc7c311f2d1f8f393efad02baa34","datavalue":{"value":{"entity-type":"item","numeric-id":5199185,"id":"Q5199185"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$DF23C24B-71B4-4874-AF40-2584B9639AE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9da42e89636c1bb7b7c39e951bb20934a0888ceb","datavalue":{"value":{"entity-type":"item","numeric-id":5370853,"id":"Q5370853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$F8BD523D-1615-4C79-B35B-F081228D2184","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba5ad8860e2dfafdd492a4ade42b23f462631c32","datavalue":{"value":{"entity-type":"item","numeric-id":5261508,"id":"Q5261508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$684D75E0-3681-4C1A-85EE-D3CBD1816030","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"804ce03be7531b05346ed40bd30dacbbe0cf6de6","datavalue":{"value":{"entity-type":"item","numeric-id":4012877,"id":"Q4012877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$F436A86D-C452-4137-958C-1F4AFBBFD88E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9bea8e9846e13a8715ab50748c9877999c599ec7","datavalue":{"value":{"entity-type":"item","numeric-id":3374913,"id":"Q3374913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$4BB9071C-F1C7-43BE-B246-7E4AE396BF5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78fdb51d791b1f89faf9b234c9f350bce2924c56","datavalue":{"value":{"entity-type":"item","numeric-id":4365732,"id":"Q4365732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$B0E68CC0-1A57-4377-8866-F265BA1BBFD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1e3b4249b8398eaf62ca99e3ad99ebe270af8ed","datavalue":{"value":{"entity-type":"item","numeric-id":3593109,"id":"Q3593109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$FAC4C3F0-7131-4BEA-886A-970C5D652B91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c00420fe303b8957df7c81923d1e72795bfd58f1","datavalue":{"value":{"entity-type":"item","numeric-id":5505517,"id":"Q5505517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$C087F992-4E36-45A2-AE72-32193A0465C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27af564deade6f382327dd892208b67d4051da26","datavalue":{"value":{"entity-type":"item","numeric-id":2988636,"id":"Q2988636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$E65B8F6B-DF52-462B-B468-0324D24C6F26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4d993f7be3ea77cad4a800be898a39b5ce70ed5","datavalue":{"value":{"entity-type":"item","numeric-id":2879246,"id":"Q2879246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$20BA603F-3D0F-4FAE-8E56-D24E7C8F4F57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bf56dec8252ad1c37ceeaafd971233e9fa863d09","datavalue":{"value":{"entity-type":"item","numeric-id":1687724,"id":"Q1687724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$46F26FB9-426C-4F80-B0C2-2D22CCA787DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"387b9b12cc18520ae469ceca2df7fe7529ab3b6d","datavalue":{"value":{"entity-type":"item","numeric-id":2829949,"id":"Q2829949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$CACB84CE-A0EC-4754-A4EA-FBD8E81E2D60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc4c2f534223ec34c41fed80e42cbca489663773","datavalue":{"value":{"entity-type":"item","numeric-id":3689092,"id":"Q3689092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$6D13FB6E-358B-4E51-97DC-DEB531CD9CB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b548fb76f8ef8a56f9223030f407f1a96f0c7ba1","datavalue":{"value":{"entity-type":"item","numeric-id":1057832,"id":"Q1057832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$8BD24B02-FAA0-4120-A520-6EB7448E14C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ddaa4e6e81660da7ff1b17a13d46308b9f0ab5d","datavalue":{"value":{"entity-type":"item","numeric-id":5395668,"id":"Q5395668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$A7CAED06-4B7B-4750-B8D0-F23D456B4FC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b798dd3085e8ee06ceaeee9f0a342b544aa6fd0","datavalue":{"value":{"entity-type":"item","numeric-id":3587439,"id":"Q3587439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$A41E954A-CB3C-4065-B846-F058C11D275B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8bfb4cfac567a097f2a651df3bdc8285a6e2cdc","datavalue":{"value":{"entity-type":"item","numeric-id":2945633,"id":"Q2945633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$779A0D45-B16D-460F-AD16-E909C67F9B29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d8e0ff8a7d0c4fc199c213531e4694eacc1d9f6","datavalue":{"value":{"entity-type":"item","numeric-id":2938044,"id":"Q2938044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$20D12C75-C73C-490A-AB93-4F0EFA48D5EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a59763b3fb25129051745803dae70f5cf79103f8","datavalue":{"value":{"entity-type":"item","numeric-id":4484343,"id":"Q4484343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$7C926C70-5829-44E7-A594-4DA3ECC8F0C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1324b3fa2ad26ee6ed29b21c5f07c23733c2a8d0","datavalue":{"value":{"entity-type":"item","numeric-id":5927707,"id":"Q5927707"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$4FF6D4D3-A700-4B1C-B894-FAD3AC9D2E02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2de4e7d4a64cec0b81a66df673db8cd9c23954d","datavalue":{"value":{"entity-type":"item","numeric-id":4178385,"id":"Q4178385"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$FE2F0169-8C3E-42F9-934E-7A32613FF9D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b559443e13096aa253418e5dea9b3753c3e0250","datavalue":{"value":{"entity-type":"item","numeric-id":882771,"id":"Q882771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$8F9F5060-9705-49ED-A8A6-299860592B6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c021bc433feaab99e85a8c56618cc75279c5f49","datavalue":{"value":{"entity-type":"item","numeric-id":2945636,"id":"Q2945636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$488924F0-A9B6-4347-B0B4-8BA859347BA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2622e8892c0aaf09e727281c5cb9109808708d59","datavalue":{"value":{"entity-type":"item","numeric-id":2988665,"id":"Q2988665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$E6DD194A-2679-438E-9F98-F5B0B38491A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50b0bfaa5604fbbf1607bb7e54efdd2fee887b49","datavalue":{"value":{"entity-type":"item","numeric-id":5327338,"id":"Q5327338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$22F71E45-DAF0-4DC1-8EC0-EBFB1D938028","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"13ffbb2a00ae3c06220852f238ea41cfa8cb8aa4","datavalue":{"value":{"entity-type":"item","numeric-id":1175940,"id":"Q1175940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$BD78D0D5-E499-4524-8040-4A41A06ADB75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22b98f4176bf7101f0a9f29100acf6c735199a57","datavalue":{"value":{"entity-type":"item","numeric-id":4779128,"id":"Q4779128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$AE89E5E0-AEDC-4154-91E3-1001C68B1325","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b731d96c6d92d6708684017ec6af996475ce74ca","datavalue":{"value":{"entity-type":"item","numeric-id":6099616,"id":"Q6099616"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$CA5DC227-32FA-4EC4-8E37-647027C1BCD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a334f4e96bc67eac9a5d7b987fa6f5d79a92b99","datavalue":{"value":{"entity-type":"item","numeric-id":2802495,"id":"Q2802495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$C5E5C773-FB0B-47C2-929D-E73F9456D8B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7efd2748f4b43f93f6c9f8888e0c86fd46d6453f","datavalue":{"value":{"entity-type":"item","numeric-id":2902914,"id":"Q2902914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$06F50B3D-7B4B-4D8C-BB5B-5559C57A114F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79fcbd1638edd3d7a428746c6ae1748ebf859c66","datavalue":{"value":{"entity-type":"item","numeric-id":2986886,"id":"Q2986886"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$BF7EC63F-D6E5-4DD6-B1A4-BB3790A825AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"856b93e25e4d1d0f8f1a57ec0b7cae72b039f6ba","datavalue":{"value":{"entity-type":"item","numeric-id":4077434,"id":"Q4077434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$2226A786-433F-4842-B38A-431A49DE11FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"436d4ddccf9258c9f31fa193f202f774ffec18b8","datavalue":{"value":{"entity-type":"item","numeric-id":1250704,"id":"Q1250704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$A5BB337D-A9EB-41FB-9F19-C732636CD9A7","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":"Q2175214$443B5337-CC5F-489F-96C1-C54931575767","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":"Q2175214$5EDE328C-756D-4432-AD9F-B4AFF6AD85BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c153f2badc3f7c7a7bdb781d3967080ef2c02ae","datavalue":{"value":{"entity-type":"item","numeric-id":5738880,"id":"Q5738880"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$8A9EAC52-9078-4058-9402-AA51F8084FCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3957ea938f58c73404c3199294aabed912fb42dd","datavalue":{"value":{"entity-type":"item","numeric-id":283770,"id":"Q283770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$13545C22-294F-4BD7-B266-B2AF5D059D2E","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":"Q2175214$4D1E7EA9-A3F0-46CA-B092-234DBD0D322C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"774c7c5e9586e81ad658f8fe2b1e3076c2f1ebbc","datavalue":{"value":{"entity-type":"item","numeric-id":5178903,"id":"Q5178903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$D149A3F9-DF3E-4208-9E25-11C56A9116A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"556222fa296f2ec2010cc38c2e35c8130f7c1529","datavalue":{"value":{"entity-type":"item","numeric-id":2891432,"id":"Q2891432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$B2279DF6-42F7-4BC7-AD96-F050623764E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"488ddf4fe425d7bd2c7abddaef1d4cbfaf0af2e2","datavalue":{"value":{"entity-type":"item","numeric-id":4783729,"id":"Q4783729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$037BAA38-FAFF-41BE-9615-EAB33B9C7283","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b75123da27aabf91573b3d0ff244451ddef0ef75","datavalue":{"value":{"entity-type":"item","numeric-id":2634501,"id":"Q2634501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$B124A188-D36A-4616-9ED7-A799239B4C47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ad91c44724a7d6cebe771b5ca37f18daf7f08ed","datavalue":{"value":{"entity-type":"item","numeric-id":4409112,"id":"Q4409112"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$8C50A02A-90ED-4EE2-BD0D-2C982B010A96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"275936cfd6130214e9d1021873d4a644d84981c6","datavalue":{"value":{"entity-type":"item","numeric-id":5398328,"id":"Q5398328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$3EAA51AC-E02C-483D-BA2F-963EB05E224F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4ef8738eccd7b653460e41e83660d0f8b8c95df","datavalue":{"value":{"entity-type":"item","numeric-id":2881098,"id":"Q2881098"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2175214$8698EFDC-81C1-4D32-B4F1-A0B2EAEB6773","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8187b8c237ce009bb2078624adce60a96f260e4e","datavalue":{"value":"10.1007/S00145-019-09341-Z","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2175214$AF86B7F8-242E-4FE9-BC7E-C3A98AF2E524","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5a9c86cfed88d5372ed769eef3623b1170b13d18","datavalue":{"value":{"entity-type":"item","numeric-id":3591439,"id":"Q3591439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"69d3a228b17997c06078b3f49afa10937db480ae","datavalue":{"value":{"amount":"+0.8360634446144104","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":"Q2175214$C252340F-D367-42BA-8D47-6C93C9005C1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"92457848f5eda64701855e3059b6522d690df072","datavalue":{"value":{"entity-type":"item","numeric-id":4933210,"id":"Q4933210"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"65ab4f41175d112edcbf2c55160f3fb357666ce4","datavalue":{"value":{"amount":"+0.8263483643531799","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":"Q2175214$01E709C6-BB37-4F8E-85B7-D77A0B84E84B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec7f0ff8f7f741216eff5ed9a84b94d54041f25c","datavalue":{"value":{"entity-type":"item","numeric-id":3503878,"id":"Q3503878"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"19fa8dee236d3177c7034ac0402beadb0c50a64c","datavalue":{"value":{"amount":"+0.8015201091766357","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":"Q2175214$BD92AEB1-046F-4D6C-B444-3BBD8F8AA093","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5cadaf031c9fd85e583aad9ed7daf3b5d8afe4a5","datavalue":{"value":{"entity-type":"item","numeric-id":5261508,"id":"Q5261508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"674d92a43e305df79203aafac9eae13eed5959bd","datavalue":{"value":{"amount":"+0.7844634652137756","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":"Q2175214$4BF4FAEB-AE43-4F9D-9A04-7DE889607E96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3fd574059b1fbf5aa99d2abc68db3d7d3fd4817","datavalue":{"value":{"entity-type":"item","numeric-id":5756645,"id":"Q5756645"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd51994cd3c2dac8c278b038044054f193b3f6c3","datavalue":{"value":{"amount":"+0.7484003901481628","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":"Q2175214$8A9AC7AF-0ED5-4D31-81AF-712D968A36CD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"CryptHOL: game-based proofs in higher-order logic","badges":[]}}}}}