{"entities":{"Q6567720":{"pageid":14178875,"ns":120,"title":"Item:Q6567720","lastrevid":103708043,"modified":"2026-06-06T07:57:36Z","type":"item","id":"Q6567720","labels":{"en":{"language":"en","value":"A structure preserving encoding of Z in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7876667"}},"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":"Q6567720$AB656E6F-4CEE-4357-B0B1-0B0D322E89DF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f22303fa45dad806d7c81f9da55c0b77999d98b3","datavalue":{"value":{"text":"A structure preserving encoding of Z in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6567720$81F8C105-3F1E-4B3C-8B2B-A756B1D16E3F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"900a82367b175c665eea0281bb3bddbb28f7451c","datavalue":{"value":"1543.68219","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6567720$BAB76CA5-3A9E-4220-AAAA-CB1FD0910A4C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0f13a55535e4249e1c3ca015ac70f30647e7b16a","datavalue":{"value":{"entity-type":"item","numeric-id":4934537,"id":"Q4934537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6567720$F2B46A6E-BFEC-4450-9E62-8CE5BF55D36B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6879ffcd1cdf9c40679b75379e38ab355a77e925","datavalue":{"value":{"entity-type":"item","numeric-id":2482442,"id":"Q2482442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6567720$1299F6DD-1E82-42E5-A4E4-AFFB89D06085","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"21d75dcb945540c248584601b42ebed5a2d66b5a","datavalue":{"value":{"entity-type":"item","numeric-id":470024,"id":"Q470024"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6567720$9676DADC-3508-45B8-98E6-F962FA81E347","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"df053448a65992a80a8bb9dc3531ec74f75059c3","datavalue":{"value":{"time":"+2024-07-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6567720$F9DD8735-FBFC-4FE0-A299-70D7A549D710","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6567720$E2C53265-7D4F-4FAB-ABEA-8291AFAD58DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6567720$D2D758EA-B88C-4E04-A331-535503FEBFCD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9065a2b15d15bfc8aaeb98db73a77ac042828cb2","datavalue":{"value":"7876667","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6567720$5B2688B7-98FC-4402-BE9A-01CB5033AA07","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":"Q6567720$DA99FD56-D847-4C53-A892-F43287DA6C54","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"35f820e9c2b45f8f035a710ad26c0ff0e5c7ae48","datavalue":{"value":{"entity-type":"item","numeric-id":3221381,"id":"Q3221381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6567720$B22C3630-55BD-4F90-AED2-68472E4EBC5C","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":"Q6567720$40F1EA50-7005-4775-A284-1FEC4903AF9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6567720$CEF65B19-C279-4822-BDA7-2E75EEC31CAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9938cbb47f6bf4773c63acc7fdc989ea1a5685f0","datavalue":{"value":{"entity-type":"item","numeric-id":4272504,"id":"Q4272504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6567720$ACE97D0E-7C7B-4193-956D-674E4F661F7C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5f99e401a7c9a933aa2431926f10dd51f43d457a","datavalue":{"value":"10.1007/BFB0105411","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6567720$0B2BD070-6273-4B67-82C9-5A90D89146B7","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d6750917f3829cc90d656580d66858111c73214","datavalue":{"value":{"entity-type":"item","numeric-id":4472177,"id":"Q4472177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"856359a4cedeed1cd501d30d3b5d8fc763fb91d5","datavalue":{"value":{"amount":"+0.8168278932571411","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":"Q6567720$8C4B699E-25C2-4C32-B646-1F411EAF65AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c09ea2c702df1394bd67a8b7e0045dc10ffa1b53","datavalue":{"value":{"entity-type":"item","numeric-id":6083696,"id":"Q6083696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a5b912e354066e903815c4b93670d61527a82d0","datavalue":{"value":{"amount":"+0.7886534333229065","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":"Q6567720$4132BC8C-E278-4506-9234-6F826034249C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce9272fab4f0ab93a022a7f20c9f6fa01a3e2d6e","datavalue":{"value":{"entity-type":"item","numeric-id":1974477,"id":"Q1974477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cc3896766024f3b7227c3cd67cc618538bb15e6a","datavalue":{"value":{"amount":"+0.7683987617492676","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":"Q6567720$B4A579EB-A907-48D0-9E20-D6055EBC5955","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e370eb66202d526cfc51dfb5304bcbdbe4c05ac3","datavalue":{"value":{"entity-type":"item","numeric-id":1974478,"id":"Q1974478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88081ac7fa8fa4a39543ebad39a3d31a381b18a5","datavalue":{"value":{"amount":"+0.7561051845550537","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":"Q6567720$8FFF8BEA-A403-4D85-B570-1E86A15F0002","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d59fffe93b8140a5662a30d8d749a62d448a0230","datavalue":{"value":{"entity-type":"item","numeric-id":1583855,"id":"Q1583855"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bddd7d75222f24d918b7fb94c845e39b9efdeb4f","datavalue":{"value":{"amount":"+0.7495438456535339","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":"Q6567720$66ADB08A-5122-4EDE-9EE3-680D21945B04","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A structure preserving encoding of Z in Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_structure_preserving_encoding_of_Z_in_Isabelle/HOL"}}}}}