{"entities":{"Q5738896":{"pageid":7768448,"ns":120,"title":"Item:Q5738896","lastrevid":52826726,"modified":"2026-01-23T14:25:27Z","type":"item","id":"Q5738896","labels":{"en":{"language":"en","value":"Mechanizing UNITY in Isabelle"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6729707"}},"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":"Q5738896$8D4AE299-2C68-4061-BBCF-AF5FF2BECB01","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3000e8c8448ec6f17ac3cac00b78d65e10cf9d29","datavalue":{"value":{"text":"Mechanizing UNITY in Isabelle","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5738896$C44115D0-8B48-4D7C-B2EC-03A837AEAD78","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c5a33394833ffb239255a438bfac038d0bfec2af","datavalue":{"value":"1365.68379","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5738896$B2F9B635-D920-4D29-B43F-47ADB9DED362","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c68113f6f3bb87c6c7b6b3710838fb36610ffeb4","datavalue":{"value":"10.1145/343369.343370","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5738896$25B486E1-1911-4BEE-BE78-5C6E7184B629","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ae5381e7211b64f5f54296c18dfaf60be613ba86","datavalue":{"value":{"entity-type":"item","numeric-id":2946565,"id":"Q2946565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5738896$7828E7E6-FB11-4086-BA22-242BF44C39FF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9fb82429bb4ba602ab7d5caf04c575952ba3fb53","datavalue":{"value":{"time":"+2017-06-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5738896$05EC090A-5328-44FA-BDBD-07C5239528CD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5738896$461A2EAB-452F-4D88-A4F2-C2C6036B97A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5738896$C47A7012-EBEB-40F2-9D3E-43399DA8CF0B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"898b25214043d6f1ccd97ac2ac7ec778d4d0dd8f","datavalue":{"value":"6729707","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5738896$7D7489A2-451F-48D0-95C7-0AE2534769EA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q5738896$0312EC6D-F84E-403B-9258-316E146AF706","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4f89702f81bb443a3353ee5f0794cae6733ae9b5","datavalue":{"value":"UNITY","type":"string"},"datatype":"string"},"type":"statement","id":"Q5738896$EBF14EC8-1AB2-4DE9-8812-4BC0C00005A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d8f9062a19f85971c14b4d71d981f064b7b13591","datavalue":{"value":"compositional reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q5738896$FC1098A2-F3C3-43DC-93E3-AE92FA729217","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"445a4fbc6b6bbba6e3c2169de8e334950d4f0826","datavalue":{"value":"concurrency","type":"string"},"datatype":"string"},"type":"statement","id":"Q5738896$BA495912-CE4F-49E2-A064-6B1852D8ED52","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"fb165e42be35cf46c1d25362f98bb10926ef6396","datavalue":{"value":"Q57382691","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5738896$3FBAAB09-0474-44BF-9954-11EA6DF1397F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5738896$09C21C1A-9A8E-47E7-94BB-4F1259789E9D","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":"Q5738896$40D39265-6EA7-4F53-BE65-60E5220AF857","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7b095eac12908cc9bdab9fb15e64495df9d2782b","datavalue":{"value":{"entity-type":"item","numeric-id":40416,"id":"Q40416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5738896$1BB3DA0D-1CA2-48F3-8782-9258C843CABE","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":"Q5738896$66D12E7F-268A-4C22-B26E-6C2DFEE5F8DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5738896$40508792-E02A-488D-BE17-064BAADA435A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"17cfe6afe68a54e81dc559ef2cd5a702765207b0","datavalue":{"value":{"entity-type":"item","numeric-id":25375,"id":"Q25375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5738896$D06AE867-B610-49F3-B4BE-7A837E7ED209","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":"Q5738896$EBE9C409-5D5C-4086-905D-EA8829F04336","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"30300f42e9e4126a0bf588688e0266af9919acb9","datavalue":{"value":"https://doi.org/10.1145/343369.343370","type":"string"},"datatype":"url"},"type":"statement","id":"Q5738896$30E623FE-4EA8-4856-B01D-E06842C91ED0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"17af06cdf2f27e0a2275f47820f4865f0f50e6fc","datavalue":{"value":"W2049023360","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5738896$0E30FCE3-DBB6-450F-AD5A-8243CEC5E4C4","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"f3e43edf426862b864fb7cb5196a7a97cb7b1a46","datavalue":{"value":"journals/tocl/Paulson00","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5738896$8C7D1C12-B477-4F94-A03D-2C721D33962B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a4b0f8fd32fb3675f59dc6402b153e97c16eaee5","datavalue":{"value":{"entity-type":"item","numeric-id":1961924,"id":"Q1961924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7b72adbda328b32bbc311b2905d0680850f7b5ab","datavalue":{"value":{"amount":"+0.8179909586906433","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":"Q5738896$C941B5C9-8398-44D6-B263-31CD14A5ACB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f74e8421eb1d50670a95fbb3e52f96306334578a","datavalue":{"value":{"entity-type":"item","numeric-id":2576572,"id":"Q2576572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8e6043ea73248b7d3505ed1cc78366cee62dc43e","datavalue":{"value":{"amount":"+0.8009761571884155","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":"Q5738896$D0DE8367-4F6F-4E95-AF97-9A22744D58D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7dc4167b85600303bf6a63862a75410108e3edd8","datavalue":{"value":{"entity-type":"item","numeric-id":4470520,"id":"Q4470520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0ebb015fed0cea55efecece454f08e12b6ff80d0","datavalue":{"value":{"amount":"+0.7919101715087891","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":"Q5738896$739B2D44-C0EC-4A1A-9312-F18FC1220103","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"53a506a732087cff0796b7307609577c09fa348b","datavalue":{"value":{"entity-type":"item","numeric-id":673960,"id":"Q673960"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c206dfc2587252b270674e2017fe2d84301cb2db","datavalue":{"value":{"amount":"+0.7828214764595032","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":"Q5738896$359D6036-2EDF-412F-973D-D84C303687A0","rank":"normal"},{"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":"f2fe6df1ea7985b2472c8636ad7895365c983933","datavalue":{"value":{"amount":"+0.781985878944397","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":"Q5738896$59FCB4D8-2DAC-4DB7-95A3-9008D1312238","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5738896","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5738896"}}}}}