{"entities":{"Q5327342":{"pageid":7356916,"ns":120,"title":"Item:Q5327342","lastrevid":51794021,"modified":"2026-01-20T01:59:33Z","type":"item","id":"Q5327342","labels":{"en":{"language":"en","value":"Mechanising Turing machines and computability theory in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6196162"}},"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":"Q5327342$8DC50CF2-61C2-48EF-BAF6-F9B832C816AB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"698871bc410b57d2db2f8a7abcc52732a9ff1b90","datavalue":{"value":{"text":"Mechanising Turing Machines and Computability Theory in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5327342$B559B89B-1537-4286-8427-1E84E3AC8E8F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"951a277f9151eb4e841f3165a590dfb9534d9f46","datavalue":{"value":"1317.68237","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327342$0CD661DC-4BE8-4B3E-9CBC-5A64140EF7EE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8269d84eab1d5124b285d19609e8ce06ca963ae9","datavalue":{"value":"10.1007/978-3-642-39634-2_13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327342$5850BD5F-2FF6-41F8-AC60-02FB2B203419","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"860f28287f925fd4b0508655be71bd25d85ef616","datavalue":{"value":{"entity-type":"item","numeric-id":237586,"id":"Q237586"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5327342$B006ED98-0A2B-4CD6-99BD-054CFC197D4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8be13823e57b532010d417bfefa3b5133f759f9a","datavalue":{"value":{"entity-type":"item","numeric-id":860832,"id":"Q860832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5327342$197777A1-4B82-44F0-931A-C90EF3527C5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8c1db257e626cb76e16153e74052c741125ca701","datavalue":{"value":{"entity-type":"item","numeric-id":2113967,"id":"Q2113967"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5327342$2AD421DF-7622-4152-AE77-CB2B44B2E4FE","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":"Q5327342$7C0CE277-A265-48AD-8ADA-7B931C3F00F1","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":"Q5327342$45A7BA5B-2A82-4B01-8D54-9AA5743B22F0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327342$88E98DFF-72F2-4EC4-8A68-4A97DC39D225","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a7dde57cbaf704d564d8f981ca98d6340e3d4aaf","datavalue":{"value":"68Q05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327342$203E7074-F782-45E5-887C-96D06F37BF0D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b1d11d2ec125c118ef0a0b17bc1ae94ce49865a4","datavalue":{"value":"6196162","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327342$24A47E8D-1C04-4A54-B6B4-E2BCEC6EF85D","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":"Q5327342$B25AF77E-EA1D-4849-A615-058526C1C270","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":"Q5327342$2B2855FF-E5B2-455B-BD87-3A1B56FF8A81","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"244af1390d64e8e93b64f5ec3e98cc6b4d9239b8","datavalue":{"value":"https://doi.org/10.1007/978-3-642-39634-2_13","type":"string"},"datatype":"url"},"type":"statement","id":"Q5327342$EC7772E3-E5B5-4750-96EA-327ABFA645BE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"01c6a00474d17df6367ff31d3a547b4faf06b9a1","datavalue":{"value":"W50191166","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327342$C0466639-4742-4C98-AB37-95855DAF678A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8c9ec596e7693236baa0e9261b42e03bd85065da","datavalue":{"value":{"entity-type":"item","numeric-id":3088013,"id":"Q3088013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3ddaaa2926e39a76048a8dcbabc3cdedf6cf8bad","datavalue":{"value":{"amount":"+0.8354412913322449","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":"Q5327342$E7EE99E4-6614-426D-A842-C989C470D84A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9027320ff90d8fe6908a21559d3d7fd996a43c43","datavalue":{"value":{"entity-type":"item","numeric-id":2915013,"id":"Q2915013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eb664754d943e0853340fb2a11042e86c8743d1a","datavalue":{"value":{"amount":"+0.8181790709495544","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":"Q5327342$AB8111C5-EEA6-4769-95F8-CEC246E0E4DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"83defe65b2cc5b3461ea6c3ebbf6d5a2bd460876","datavalue":{"value":{"entity-type":"item","numeric-id":744986,"id":"Q744986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f3f630a9aa802ff337667aee1f323c61564bde82","datavalue":{"value":{"amount":"+0.7689869403839111","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":"Q5327342$0EBB9582-4C1A-48FE-BA1C-680C0B10F2A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aa4c65573320df4f4f50c0e731042082b7e7a270","datavalue":{"value":{"entity-type":"item","numeric-id":2797865,"id":"Q2797865"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e1d4671e4f12a5f796097313c7b868a0da1a04c1","datavalue":{"value":{"amount":"+0.7659655213356018","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":"Q5327342$4310201E-589D-42A2-8053-F137FD9C428A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18f8fb547a6e03c53dd6413528e41785493e63a7","datavalue":{"value":{"entity-type":"item","numeric-id":2879266,"id":"Q2879266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3823855fe29f0f6c47213e2ad7060911e1a21beb","datavalue":{"value":{"amount":"+0.7387493252754211","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":"Q5327342$5BA492FD-DA6B-4C1B-96CA-2E1EE01AA69B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5327342","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5327342"}}}}}