{"entities":{"Q3055747":{"pageid":3066463,"ns":120,"title":"Item:Q3055747","lastrevid":51127271,"modified":"2026-01-16T19:59:13Z","type":"item","id":"Q3055747","labels":{"en":{"language":"en","value":"Unifying theories in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5814099"}},"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":"Q3055747$508F1FEF-8C06-4FE9-AA15-B59A22BB70D8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6053ab75b7f95a991f7275e7a73569e69672ed8a","datavalue":{"value":{"text":"Unifying Theories in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3055747$9A40BC29-6E93-40D5-93C8-D251952A8CF7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2fa02318e42e17416ab4cb21107672a888efb199","datavalue":{"value":"1309.68045","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3055747$A53CAA8A-336A-451C-BA1B-D7BC29CF164C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b1f824a1b1f58ee665582faeb1a507972e82aaf3","datavalue":{"value":"10.1007/978-3-642-16690-7_9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3055747$5909A3FC-C124-4620-A493-78505238A594","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7339e4482cefbc6dca0b6997c5f307bd3d3e730f","datavalue":{"value":{"entity-type":"item","numeric-id":3055746,"id":"Q3055746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3055747$14083BA5-8271-4BB7-B9B0-718502A50D40","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":"Q3055747$BBD9AEF8-7C5B-47DB-BEC4-7E849A8D8FAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fffd81c6aae76a5fc581ab482db7fffc27874219","datavalue":{"value":{"entity-type":"item","numeric-id":391417,"id":"Q391417"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3055747$2205183A-2AAD-401C-BC81-2AE88F7C140D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a469690149bc3cf60335251215f8201e92d3e50c","datavalue":{"value":{"entity-type":"item","numeric-id":2814611,"id":"Q2814611"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3055747$9F71E231-A088-4570-B278-B8DA1BB2A5D0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4cb643977987b416fd9b27db151f69ce02967bfa","datavalue":{"value":{"time":"+2010-11-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3055747$A2D78067-632A-47BA-A6FB-F132132B8DDB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3055747$C0426968-F393-4475-B12B-9D112E0FE702","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3055747$0C643194-945A-4F72-B104-A8FBDDFF3F69","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1a261eb9aaa928deb98eda51f099af8ac539237f","datavalue":{"value":"5814099","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3055747$08CD40A4-8CEF-4C6E-9E01-54B14AEC694F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"03a0d2848f7e13e5373d661d808855d0d8662087","datavalue":{"value":"UTP","type":"string"},"datatype":"string"},"type":"statement","id":"Q3055747$F3E2D345-7737-4F6D-AF53-769F570ECEAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3055747$E689E410-BC0A-45A7-A289-11497CC2508C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q3055747$14E75662-171F-43EC-B1FD-BA4C563E2481","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cb1658b60e766a02ebffc17e47bf24ae50d17b7e","datavalue":{"value":"CSP","type":"string"},"datatype":"string"},"type":"statement","id":"Q3055747$144F5D74-E46F-4075-8676-31265DF21F72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a6c8223143402d63869cb92db7f64e9cbcbc6f9c","datavalue":{"value":"Circus","type":"string"},"datatype":"string"},"type":"statement","id":"Q3055747$C914A897-B288-432B-B9AA-9114281442CE","rank":"normal"}],"P1463":[{"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":"Q3055747$8339201C-977D-4B56-9ED5-BF6B20336B1D","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":"Q3055747$5560575C-87C2-449C-8A10-48FB5C112E26","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":"Q3055747$FF714C13-6E2A-4D91-A5C1-10E4354463FE","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":"Q3055747$5EDF2A5F-5C2B-46A0-A4E2-9B893CCD956F","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":"Q3055747$010022C5-9C9B-4EC0-AD03-CEC85E64A8A9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"aa4a309c87c4f494d418bc0e273cc673de94dfeb","datavalue":{"value":"https://doi.org/10.1007/978-3-642-16690-7_9","type":"string"},"datatype":"url"},"type":"statement","id":"Q3055747$C6FC6D6F-4516-4D7E-B30C-92E94380769A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e21a4a23c82d22798156fe448f04daf6bbee6247","datavalue":{"value":"W43811100","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3055747$5159E2E6-8801-4CD7-A8B4-54E4A552EE28","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6442d5e89d0411d47ef58a6a762b691cfeb68bf8","datavalue":{"value":{"entity-type":"item","numeric-id":2948230,"id":"Q2948230"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"65f2c6927884261896b05425e51351d3eb6bae25","datavalue":{"value":{"amount":"+0.8496675491333008","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":"Q3055747$31E1084C-45BC-49E9-9404-E6C894F08B60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d6db23d2ad35e7f6579e9dc67d88087dcc91726b","datavalue":{"value":{"entity-type":"item","numeric-id":2814613,"id":"Q2814613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"18323ffebf78ce44f87887659726868541b7a249","datavalue":{"value":{"amount":"+0.8321158289909363","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":"Q3055747$121C9168-E04D-4DA9-8DC3-1B1F3104C86A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"916f06100b463e92c67a400ec913503d255e1185","datavalue":{"value":{"entity-type":"item","numeric-id":1708708,"id":"Q1708708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53940210dbd0cd0835a4daaa2582f2412e369a61","datavalue":{"value":{"amount":"+0.8117825388908386","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":"Q3055747$68F7B7EF-3774-45D7-A832-A49D85F41F67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a882b9f94d2d662fc1bfb61a704bef560732636","datavalue":{"value":{"entity-type":"item","numeric-id":436368,"id":"Q436368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"76917d660ae7087c7c828c4e50d6aefea5578f30","datavalue":{"value":{"amount":"+0.8017162084579468","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":"Q3055747$9DD0246D-9413-4652-96B7-526BF6699287","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5841d5f9923d6922c7afdd94dd1a26555046af11","datavalue":{"value":{"entity-type":"item","numeric-id":2971180,"id":"Q2971180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8e745c8473004fd7c5d3922a11b9ed209725fca5","datavalue":{"value":{"amount":"+0.794994056224823","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":"Q3055747$86B49785-9C49-44A3-8669-3240059A79DE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3055747","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3055747"}}}}}