{"entities":{"Q2128789":{"pageid":2139532,"ns":120,"title":"Item:Q2128789","lastrevid":54301973,"modified":"2026-01-26T14:44:53Z","type":"item","id":"Q2128789","labels":{"en":{"language":"en","value":"Beautiful formalizations in Isabelle/Naproche"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7511923"}},"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":"Q2128789$D104DCB2-5299-448E-8A93-C669A6EA89A0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ee09d68784392e106183ebbb65436eccd1022985","datavalue":{"value":{"text":"Beautiful formalizations in Isabelle/Naproche","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2128789$10F68079-7AC4-4FF1-9C71-B2FCEE12DD24","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"50f16427cd6f0df58fa13586fdc33832ca065d6f","datavalue":{"value":"1485.68290","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128789$07DBE325-6139-4676-BEF7-4A2E6B57394B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"89a9f4666327177ae19c1eed7982cf83bfe793b9","datavalue":{"value":"10.1007/978-3-030-81097-9_2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128789$F013DE89-648C-4D7A-BF57-3266CF87A0FD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6e5ef3c09dbe743228f36a4d9b380063a6dc6203","datavalue":{"value":{"entity-type":"item","numeric-id":2055895,"id":"Q2055895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$E31D9607-169C-4E24-A069-DD4E643BE030","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"97d0b9b61d83d1e98f6242a5df0440e02577e539","datavalue":{"value":{"entity-type":"item","numeric-id":375822,"id":"Q375822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$22EE435B-9841-4F59-B468-D7F59CEE7BE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"87159b4f68d14237460a9d9df76f5a804b76cde2","datavalue":{"value":{"entity-type":"item","numeric-id":2055896,"id":"Q2055896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$47576D0C-0F2D-4517-A040-3BF9150E0576","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cc28df9555a9803a43ddbbec457bb58b52f60ca9","datavalue":{"value":{"entity-type":"item","numeric-id":2055897,"id":"Q2055897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$F9F77EF5-5A3D-4942-BD59-62989ADC0901","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1739a6cc2bec4304864e33cc6d227647838111a1","datavalue":{"value":{"entity-type":"item","numeric-id":2055898,"id":"Q2055898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$17AFF087-58DB-4D30-AEE4-7A4B482962AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4dd54c36dedd3db2e4116d4d72ec5108e3311038","datavalue":{"value":{"entity-type":"item","numeric-id":2128788,"id":"Q2128788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$CCDBF6E8-6B2B-4C84-8D8E-61329494BA34","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6a2d220bbda83e730799716cad61153265e68ffa","datavalue":{"value":{"time":"+2022-04-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2128789$B6B29C50-638B-4B41-B56C-A42194D3B316","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128789$72108948-A99C-41EC-8F86-DAF39BFC4472","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9d18eab5e457188f13453c480b60f27a8a86c0bb","datavalue":{"value":"7511923","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128789$130F57B2-9CB0-4930-8E94-9855C99C021E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6185d1a6f6936c9abdfec8ede6c22f4a1cb47d10","datavalue":{"value":{"entity-type":"item","numeric-id":5974382,"id":"Q5974382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$69E41A5C-FEA3-427E-9735-54C374301F2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"338aa0d01ce8385e92ab151731f9345a1bd5e9d6","datavalue":{"value":{"entity-type":"item","numeric-id":3107050,"id":"Q3107050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$69EA3C61-5494-4AAC-978B-48A189E5957E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ea1145a6252ac1c2f0190a1ae918e36f86e8df7","datavalue":{"value":{"entity-type":"item","numeric-id":4340904,"id":"Q4340904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$B4473D98-067A-480F-913E-6A514CC0FA44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae5be7a3a808b40ac414736b090a7ceb254afa74","datavalue":{"value":{"entity-type":"item","numeric-id":2965620,"id":"Q2965620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$02D0B52C-E770-4497-9AAC-D0797BB1E548","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3dd33855336399d060e4c0008afb085c9559eabd","datavalue":{"value":{"entity-type":"item","numeric-id":5747782,"id":"Q5747782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$39AAE1ED-72A3-4625-90D0-50FAFE66A442","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"388652312846c036177579ce98da69efc177622f","datavalue":{"value":{"entity-type":"item","numeric-id":5902174,"id":"Q5902174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$BBF1C517-F4AF-4AF8-B0A1-EFA7FF454AB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"24a7db326e43376dc12c8369f0aa456c47e285a4","datavalue":{"value":{"entity-type":"item","numeric-id":1297036,"id":"Q1297036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$5070E43F-CF33-4FED-921E-9A0939F042B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e320d5ab20d9378e83c08a862b63bf2725892d4a","datavalue":{"value":{"entity-type":"item","numeric-id":2653567,"id":"Q2653567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$2987D3B6-8F1B-454C-9AD6-6C9156836EE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5b79119f9505990ffd9f1c920604fb44a0b0165c","datavalue":{"value":{"entity-type":"item","numeric-id":3608785,"id":"Q3608785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$E3EB49BB-2328-4096-A67A-13E171543423","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d1dd217b6d60cfd1c7517ad3aa621ccbb5c7c91","datavalue":{"value":{"entity-type":"item","numeric-id":5505538,"id":"Q5505538"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$8611994E-6E60-48A2-AD79-3D613AE20C21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6b3c86719beffa574d5754bc195ec31b1274957","datavalue":{"value":{"entity-type":"item","numeric-id":2443390,"id":"Q2443390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$15A7A052-B80B-4A22-A1ED-4C6E9D197D5D","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1854721036cb61f11d38bc9b83f78dc8d1e1b816","datavalue":{"value":{"entity-type":"item","numeric-id":5974382,"id":"Q5974382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$26600C11-A6DB-4FAE-92FF-2B793744FA74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dec9660857c05980e3c0b17c51d483bf1a29e419","datavalue":{"value":{"entity-type":"item","numeric-id":40021,"id":"Q40021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$8232D59F-E8E8-4DC6-AD1C-F4A3C204AD60","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":"Q2128789$F78FC359-A191-4067-BD3A-8DAA790B0A52","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":"Q2128789$53F2C53C-CD9E-45BA-8E4E-352AA7128E96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a3e24b1e555719d904bc5723d040851bdd6284eb","datavalue":{"value":{"entity-type":"item","numeric-id":21775,"id":"Q21775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$FBFF2124-D75A-4CA8-9CD9-33F1DEB5A6FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"91b852acc0d0dcb394ea74c8e76a901ae0257702","datavalue":{"value":{"entity-type":"item","numeric-id":21776,"id":"Q21776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128789$0D79812B-27FC-4835-8B59-03CAEC5AE78B","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":"Q2128789$C7690F57-A094-41DA-9863-AC604396F471","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"428d432db52ab05682236dc1da210174bdfe2138","datavalue":{"value":"https://doi.org/10.1007/978-3-030-81097-9_2","type":"string"},"datatype":"url"},"type":"statement","id":"Q2128789$4951C5F4-F94C-4B43-B6ED-BB9F319A3B2C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"aa988caff384c82391bf5971107f7af084b5efb8","datavalue":{"value":"W3184839407","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128789$B7A390F1-851F-4CD3-A1AE-E1A664579E31","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85f5a712434b519e83eb4cd0655faaf4a1e99d17","datavalue":{"value":{"entity-type":"item","numeric-id":2219411,"id":"Q2219411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bfb0b41ed259822250c83cc9da10514672ded101","datavalue":{"value":{"amount":"+0.7720075249671936","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":"Q2128789$31E92834-2227-4A16-B4B1-5387733F9270","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"060565dc962325d9cae604367018fca0b1002877","datavalue":{"value":{"entity-type":"item","numeric-id":2657827,"id":"Q2657827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"05888fad19358f44a8fab1afeca2abb8215a46ca","datavalue":{"value":{"amount":"+0.742100715637207","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":"Q2128789$7D31FD46-71CE-4D21-B2D1-32C6D5CDE5EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a7d172aafc633ac2ef616f053ae812d725c9f851","datavalue":{"value":{"entity-type":"item","numeric-id":5505517,"id":"Q5505517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fd97488ab93dfd9aef8c9d5ee555ce4727d813d4","datavalue":{"value":{"amount":"+0.7342101335525513","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":"Q2128789$6AA897AF-24DF-4F54-8C42-50DBD9A74BC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c1fbe8f76631e9b24e2621b72c3ad8cc01fc1fd0","datavalue":{"value":{"entity-type":"item","numeric-id":1868515,"id":"Q1868515"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e2244c01a370d64630655d829e190d3748f54f71","datavalue":{"value":{"amount":"+0.7293225526809692","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":"Q2128789$23B0CCA7-532C-410B-98FD-09C70AD59F02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a3ba4593734f4ebe3888f6b04d2e76479668adc6","datavalue":{"value":{"entity-type":"item","numeric-id":2845528,"id":"Q2845528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"15012054dbfe82f85597e64f560327137edd17b4","datavalue":{"value":{"amount":"+0.7292467355728149","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":"Q2128789$AA2F0502-69F3-4692-85F2-1A5EF215E403","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2128789","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2128789"}}}}}