{"entities":{"Q1739913":{"pageid":1750655,"ns":120,"title":"Item:Q1739913","lastrevid":68872086,"modified":"2026-04-13T02:47:18Z","type":"item","id":"Q1739913","labels":{"en":{"language":"en","value":"A consistent foundation for Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7048643"}},"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":"Q1739913$54ACD0D2-18C3-4C49-906D-C7EB1D882CEA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d2e3fa0f354fa2da657c9c5f649ee2a186f1c858","datavalue":{"value":{"text":"A consistent foundation for Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1739913$D549B960-63C4-4133-BD47-7C11CF224B0C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2d91fd51c1ef460e365acd50afa856fb3ff34a76","datavalue":{"value":"1465.68289","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1739913$0754810C-DBD2-4BE1-A939-B6DDAC0205F7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb18cf0542c9d5785b9c3d13ac135abc8a7efb68","datavalue":{"value":{"entity-type":"item","numeric-id":1687532,"id":"Q1687532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$2BB7CE23-FDDF-4617-B849-5F8DC25D8461","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2ef4ea61388b67726824db4b9b444c6863305920","datavalue":{"value":{"entity-type":"item","numeric-id":817686,"id":"Q817686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$5CA1C9AB-9085-4CC3-B6CD-0657BAA4FDD8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$F450280D-FA33-4035-913E-1D9B94CF4118","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c886460d86f543351b8f7fb5093933ac0a350b03","datavalue":{"value":{"time":"+2019-04-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1739913$35233D25-A6F4-4B97-9751-E1039FD0F17A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4a506eaca38239289a2480cea5ed3d2ca331c519","datavalue":{"value":"https://eprints.mdx.ac.uk/16073/1/isabelleHOL.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q1739913$48506D22-B879-4889-8AC0-18901E7975D1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1739913$3FDC8DDB-424F-438F-B278-7787B00F1A2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3f6d4b3012578fba2d8ab6b9e39d328cad9def57","datavalue":{"value":"03B16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1739913$9479B298-E46A-408D-BE3D-480F9792244F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1739913$72A5FD40-4953-4B9B-8AEA-9A4540B10DD6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"78c6f0692e399854634321c3ecf53d251827121b","datavalue":{"value":"7048643","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1739913$44535171-E326-4980-A0E4-2EA60047A14B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1739913$74E1C700-2B38-4EC9-9837-463E5B489D0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1739913$6B53156B-85AC-4907-8CA9-40DD7DCB701D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q1739913$E670F989-DF3A-4E87-BC8B-D690C1F46BAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"52c2513afc8941299b07e63a5555cd1e7cb85f4a","datavalue":{"value":"consistency","type":"string"},"datatype":"string"},"type":"statement","id":"Q1739913$4E4DC5DD-E4B5-4DCF-AB82-6A14F5E7656E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0d1a530ebebfe9d67cc01e23074092169ca8f759","datavalue":{"value":"model-theoretic semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1739913$C7A97057-E750-41B6-89B1-1C105E76ED95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"32d8238487adba1a2357256e7ad25fd8405dac6a","datavalue":{"value":"ad hoc overloading","type":"string"},"datatype":"string"},"type":"statement","id":"Q1739913$5E94DB12-4B9D-48B5-997A-7A807D8B260C","rank":"normal"}],"P1463":[{"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":"Q1739913$B8BBB2DE-BC74-4C08-BB9B-D464C87ABC29","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":"Q1739913$1064DD78-0813-477B-A343-D16316B19C73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$D1AD34C2-DDBF-4828-8C48-43F6305111EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$472D63B7-5D72-4297-AC0B-B43F72CAE3A0","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":"Q1739913$D95B4071-F6F2-45D8-B9E1-607F4C004E6F","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":"Q1739913$B264FA44-7F13-4C9B-9163-1B9083AEF0AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcaf3b20cd7fd897f2f47a708bad9d4f554cb6fa","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$A2443A04-1670-4E28-A87C-7DA190E4704D","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":"Q1739913$08EACDDA-FEFA-45F1-9324-C08E09C71295","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$A2FB9314-DE3C-4943-83DC-0A25BD39829D","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":"Q1739913$A4E2108B-2A54-474C-8EF3-9E1D57AF9001","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8b2040a476017b43b21bd352cfec0a67d631d6d4","datavalue":{"value":{"entity-type":"item","numeric-id":18467,"id":"Q18467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$FC1A8FFB-5E2C-48FE-BDDB-27BF9BEB6F76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e079f4640d565f0ca1930fd327c2c7e8d634508","datavalue":{"value":{"entity-type":"item","numeric-id":21954,"id":"Q21954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$9B30A174-AAAA-41C5-8F93-9074B4B747DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d40b61763c81cd80c5c82e03c39b2fdb5cbb80a2","datavalue":{"value":{"entity-type":"item","numeric-id":23989,"id":"Q23989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$37A44589-970D-4930-B5C8-9F0659E30A93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"44e192ea0614ca90dcab29c306f09db708056c50","datavalue":{"value":{"entity-type":"item","numeric-id":24736,"id":"Q24736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$F6495012-B2B0-44B3-B8BE-7E71C05FA9ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"468fad61234030d4d4bd64e4991e6e30fb2af1d0","datavalue":{"value":{"entity-type":"item","numeric-id":29451,"id":"Q29451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$0D444878-3716-4557-ADE0-CC5E29846DAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a4586214c0d20ff9dc4c805490542b3e8ff1c709","datavalue":{"value":{"entity-type":"item","numeric-id":40952,"id":"Q40952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$7F55B4B3-6E61-4C63-9A0F-6B266A4BE953","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":"Q1739913$9269F24B-B4CE-456B-AC71-31163244C83B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fc9d931dbe7672c43f77e2f10dbe5bf651d738d9","datavalue":{"value":"W3023928742","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1739913$90124DD2-F75F-4F35-9A6B-19E87B7D23E1","rank":"normal"}],"P223":[{"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":"Q1739913$90E3D420-9D57-4585-A616-C99042328A6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9864722e1120856743b1e5eb3761fb8bcb430e4","datavalue":{"value":{"entity-type":"item","numeric-id":2879241,"id":"Q2879241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$83C1578E-7EBD-449B-B203-D71A71B6F8A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"739330a58a3c3aae77075c5fb847ca13d50160d0","datavalue":{"value":{"entity-type":"item","numeric-id":3075242,"id":"Q3075242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$07FD3B9A-3D79-495F-994E-95DA2214177C","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":"Q1739913$3D445473-2B6F-4E6B-B0E9-71B660CBEA01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60ec34bc45b3dd9208c19ebd43163fb16d3d98f5","datavalue":{"value":{"entity-type":"item","numeric-id":2981955,"id":"Q2981955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$B1CB8627-64C8-4D51-B4CB-A35132282A3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1903be4a36187a0a0e197e708bc72f62f93b28bd","datavalue":{"value":{"entity-type":"item","numeric-id":3183520,"id":"Q3183520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$5C68078A-9BD8-4FA3-8CF1-8285F5D5C27F","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":"Q1739913$783F163C-079D-4F48-B363-8DB788DE339B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb1bab11b75e766c233c3a1b9a3682b90b0e288d","datavalue":{"value":{"entity-type":"item","numeric-id":3075247,"id":"Q3075247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$E843FA5C-ECBF-458C-A84D-615BDDDD39BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14533123e0b9e73c06f9737a070ee002c25f5f1b","datavalue":{"value":{"entity-type":"item","numeric-id":3612442,"id":"Q3612442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$D35AE8FC-7136-4623-9858-A761CCB2B554","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aeedc506ee95714a79cfc16f82862182df8774bc","datavalue":{"value":{"entity-type":"item","numeric-id":3613408,"id":"Q3613408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$9C2E5781-5EFB-41F9-8152-3F09ED6846FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d360f4c10b4163627f57faa3db163275ea6a011","datavalue":{"value":{"entity-type":"item","numeric-id":5327350,"id":"Q5327350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$113BC64F-BE37-4DEF-B960-F90755DBF3BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8a7e549f0fba6b332f88c2b3d15bc37b5e90f37a","datavalue":{"value":{"entity-type":"item","numeric-id":5747640,"id":"Q5747640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$EEC090E4-C92C-4F16-991B-F1171CD97E28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67c913a72527b57ea467866b24b8cfd23fe78226","datavalue":{"value":{"entity-type":"item","numeric-id":5747659,"id":"Q5747659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$322DC8F9-A013-49D7-A79A-FC4F49B88904","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"999b14224255809098a606c16262602638de58e6","datavalue":{"value":{"entity-type":"item","numeric-id":2879260,"id":"Q2879260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$A0D70374-7F74-496A-BE22-F03EF4981950","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":"Q1739913$30FD9687-193C-4335-80DF-1F84679E3811","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7a1ce015f9a6115f5e15ce96a4b6a73ac4d89f9","datavalue":{"value":{"entity-type":"item","numeric-id":5327340,"id":"Q5327340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$FD095EB0-ED28-42B4-9310-01A2FF2D095A","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":"Q1739913$9C80515F-C74A-4F03-9ABE-415DEFC2996D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac497f626b608c6620476476c3df0e4c5760d79d","datavalue":{"value":{"entity-type":"item","numeric-id":2879267,"id":"Q2879267"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$2E6FC21A-4B48-4F3F-9FA4-B98F50A0BA8D","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":"Q1739913$C1CDA17F-A9F1-470B-A2AD-83010500BCAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34cc3a3d8722bafd75712de0bd470daeb53e5397","datavalue":{"value":{"entity-type":"item","numeric-id":3527296,"id":"Q3527296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$F1EE96A1-428C-4638-8808-73F64D2C209F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ff7181965704e473c064c7d95f9f7f0b397f93f","datavalue":{"value":{"entity-type":"item","numeric-id":3543665,"id":"Q3543665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$99E8E0B5-C263-4FA2-9EB8-7EE26A638718","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4feea37c535bd22cbdd726fd39655db123c9a3f5","datavalue":{"value":{"entity-type":"item","numeric-id":928672,"id":"Q928672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1739913$632577AC-5C51-4065-991A-A8683322C54D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"10e5a8b79309339485462941516e5e7616b6e9ad","datavalue":{"value":"10.1007/S10817-018-9454-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1739913$26CD653C-7EAB-4062-81E0-B207F8382850","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"19914ff8362a88c613e25c3bea458e1c7b08dd0c","datavalue":{"value":{"entity-type":"item","numeric-id":2945636,"id":"Q2945636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a21d4c644640581fcad94477a2d2ec1282142137","datavalue":{"value":{"amount":"+0.9992675185203552","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":"Q1739913$DAF5C81B-EA0C-4782-BDC1-B5E610582C1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3bab036782718245d05f152a7e71f8f232957e26","datavalue":{"value":{"entity-type":"item","numeric-id":2988665,"id":"Q2988665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"19c2e67dbdb94268e54fd0148a2bd76318a68110","datavalue":{"value":{"amount":"+0.8843828439712524","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":"Q1739913$0D56591D-F8BB-4705-9C84-EB0EF7FD84DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f486f15bb96c9d702825bb4445acddcc63515c3a","datavalue":{"value":{"entity-type":"item","numeric-id":287358,"id":"Q287358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0926e30a1347a4a1dd3659b730a0ba6a41bb8172","datavalue":{"value":{"amount":"+0.7774130702018738","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":"Q1739913$A8AC7263-420C-4895-9DDE-E5F269CE7CD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6e66700aa57a71e967e8560ef8d8dd1126b71213","datavalue":{"value":{"entity-type":"item","numeric-id":3527296,"id":"Q3527296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dbafd43e26097662869f908056381bfc67e96d47","datavalue":{"value":{"amount":"+0.7645636796951294","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":"Q1739913$36708490-88F1-484D-97C3-9A3B924D1B0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0233b2749ba68d2e1c3ea350d744b8b261347aa3","datavalue":{"value":{"entity-type":"item","numeric-id":2333319,"id":"Q2333319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a1079a611245dd4e4d3d874702dbc42cd79c4fce","datavalue":{"value":{"amount":"+0.7449705004692078","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":"Q1739913$EE7480AE-76D0-432F-BD93-7E97487DA1C7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A consistent foundation for Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_consistent_foundation_for_Isabelle/HOL"}}}}}