{"entities":{"Q5327339":{"pageid":7356913,"ns":120,"title":"Item:Q5327339","lastrevid":51794009,"modified":"2026-01-20T01:59:31Z","type":"item","id":"Q5327339","labels":{"en":{"language":"en","value":"Data refinement in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6196159"}},"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":"Q5327339$A2E8AF2C-6532-4F6C-AAEB-7A77D12ECF92","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c5a27d593a549ba9c81bc3f91b4da324d7801cd2","datavalue":{"value":{"text":"Data Refinement in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5327339$B9651753-6FE9-4901-9871-84B66463F982","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b40ee7f39f33d641f7c592d741527aa38bf87024","datavalue":{"value":"1317.68212","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327339$2964AE70-8CC4-474B-9CAC-ECEA1A440FCE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3835aaad374fce90f45852aaaa4c1ceaab24ca56","datavalue":{"value":"10.1007/978-3-642-39634-2_10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327339$2DA609DE-CC02-45AA-AC4A-6353F8553829","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"834e780fa83e41c00339343618afecbdebf7a197","datavalue":{"value":{"entity-type":"item","numeric-id":2913942,"id":"Q2913942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5327339$F8E7FE1F-3D2B-4624-99B8-ECD2C1227076","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":"Q5327339$669DEB04-E94A-47B4-A275-83C92667E391","rank":"normal"},{"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":"Q5327339$A9CDBBB5-A311-43D4-947C-36BEC177BC45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bd39997decddd4925a8ef09cbbffc4f41d2b1f00","datavalue":{"value":{"entity-type":"item","numeric-id":670700,"id":"Q670700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5327339$450E7367-A6BB-4988-8A25-695079A0B91B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5327339$E5A432A4-1403-43A4-9C50-A38FFF78E969","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"00eca6587536a1681b3f41d63f34e248b2e37166","datavalue":{"value":{"time":"+2013-08-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5327339$7FF374A4-21D1-4A07-8F4C-EFD167A1ADFC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327339$E0BE81B0-C8E8-4939-930E-6BD1DD31A314","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2fbd2b77cd97b3d23c242872f054dc64bb4d1eed","datavalue":{"value":"6196159","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327339$8C320CDB-E9CF-40F7-BFF5-446854F413D3","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":"Q5327339$5F5D3E47-C5D6-4E9F-8553-211EA3F177A5","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":"Q5327339$43BF5331-13FA-4CBC-AA8B-11D8130F30A2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"34c795ba08b99cd0b1872fc542ec72fcaa1ab8b3","datavalue":{"value":"https://doi.org/10.1007/978-3-642-39634-2_10","type":"string"},"datatype":"url"},"type":"statement","id":"Q5327339$5C7CA6C8-2B11-4D54-B1D9-EB86F0A4CCFC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"953247b2f22a9741205774671805777302e520cd","datavalue":{"value":"W1713610","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327339$B48F9171-2815-40DB-9303-6B0077ECBF86","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"945512cd015e02b0cb42f8b2229b6e8d43e324bd","datavalue":{"value":{"entity-type":"item","numeric-id":5327338,"id":"Q5327338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"36a3ffb755a2776d88162c50e5fbc82730d4a232","datavalue":{"value":{"amount":"+0.8262697458267212","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":"Q5327339$2AFDB543-BB83-4DE0-A9E4-654B92E41CCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"805759e12df01396966f318736496b4454741829","datavalue":{"value":{"entity-type":"item","numeric-id":2417948,"id":"Q2417948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"35d2b7067ee2fd926553bf60cddad811860b80c4","datavalue":{"value":{"amount":"+0.7837068438529968","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":"Q5327339$D91A80B3-94B9-420D-B366-2CC38874176B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8059791974458f7341678f903beedafe125598c5","datavalue":{"value":{"entity-type":"item","numeric-id":2914741,"id":"Q2914741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e4917c337872299d5ee7bf1d29c06d6b22768a32","datavalue":{"value":{"amount":"+0.7805875539779663","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":"Q5327339$6A43AE9E-E70A-4A6C-98D8-297C58E3F153","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"959be19baa4476667a8bf253e7c26f9c31eafdc1","datavalue":{"value":{"entity-type":"item","numeric-id":2945637,"id":"Q2945637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"257ce55e4b7d0dca998eaeeb6b85620ce3eddc7f","datavalue":{"value":{"amount":"+0.7669458985328674","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":"Q5327339$B29768F1-0B98-45F3-B77F-959FE5F055F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f06ce394d56681f16987829d5518799d1c8091e1","datavalue":{"value":{"entity-type":"item","numeric-id":1739909,"id":"Q1739909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c583ee83a7bc89a336c7eea9accc1bb6b8e65bb","datavalue":{"value":{"amount":"+0.7638428807258606","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":"Q5327339$8AA53CDC-6185-4821-91EA-C31D77AA1C5D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5327339","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5327339"}}}}}