{"entities":{"Q5170238":{"pageid":7199810,"ns":120,"title":"Item:Q5170238","lastrevid":52046336,"modified":"2026-01-20T20:06:44Z","type":"item","id":"Q5170238","labels":{"en":{"language":"en","value":"Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6319598"}},"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":"Q5170238$3CC23BC3-DD5C-4D05-B77D-43CEBB52C7F0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"403c505bfe6a22b7fb6eb2c68fecf85d45be97a9","datavalue":{"value":{"text":"Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5170238$4B93FDD4-E6E7-46E4-9CAE-D96834DD0F87","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ed476d99fdd87b1fe66ef7656314941e077260f6","datavalue":{"value":"1294.68129","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5170238$A6F9A5B1-117B-438C-8E01-18963D31348E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a162d67ca0f0da05fadb758011f7efa5d1e07db6","datavalue":{"value":{"entity-type":"item","numeric-id":287364,"id":"Q287364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$9B8ACBDF-A2DE-41CD-9D10-F79E7B3D1B55","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$ED838371-E816-4863-8D01-B8170D10166B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ccf050e1c17ecf8d76a38048fff5f6c3dcd9c662","datavalue":{"value":{"time":"+2014-07-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":"Q5170238$85276B14-815D-4FD4-B509-1F38BA1AF7EC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5170238$A258898E-CFA7-4A84-89B1-042729BEBA49","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"45a552476445c4c1ecc18fc35ed9971e443d8aef","datavalue":{"value":"6319598","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5170238$97E0881E-36F0-4125-92CE-726E8D204C18","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q5170238$B470E409-473F-4131-BB33-C538B613BB89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"34ed4687cce651929f9e5e5114db76a2b5f7c532","datavalue":{"value":"Scala","type":"string"},"datatype":"string"},"type":"statement","id":"Q5170238$CC8B4C34-96E7-48CB-A21D-904276416DC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"61da1432ea11a12fb7b5f1e67e32e3b9ee07813c","datavalue":{"value":"jEdit","type":"string"},"datatype":"string"},"type":"statement","id":"Q5170238$4BCF2CDA-7277-482B-8D49-F140E2932B78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"146414f550eb9346a1586996000d53e192311b6b","datavalue":{"value":"asynchronous proof processing","type":"string"},"datatype":"string"},"type":"statement","id":"Q5170238$3831A8E9-42D7-4367-AC80-764B18345923","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"143eb41e5522f38520e2e72a1fdaa74b5eade73e","datavalue":{"value":"re-use of editor and IDE frameworks","type":"string"},"datatype":"string"},"type":"statement","id":"Q5170238$F7C64EBE-F105-46FC-B791-CED52D653D50","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f47f15b92e642401330298216eda9b5ac94cc191","datavalue":{"value":{"entity-type":"item","numeric-id":38277,"id":"Q38277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$06C36F59-0933-4FE5-99A8-61843F04E07A","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":"Q5170238$27228512-CCA1-4C85-A4A0-DA47290B8E4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$D5D838FC-4503-46E1-A752-9888F3DE9DAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9aeef25d5839625565921d83cf1c652bf6f2fbf6","datavalue":{"value":{"entity-type":"item","numeric-id":17052,"id":"Q17052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$4BD0B09A-D060-421C-970D-EE47B5A2BFAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"854b234eb9a95f8c5e737feeb323e817bee5cabc","datavalue":{"value":{"entity-type":"item","numeric-id":19233,"id":"Q19233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$60B4B2D6-48AE-4431-89A9-79520B621F46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e262f47aa23786f0d5ca3c491b5060c53e80792f","datavalue":{"value":{"entity-type":"item","numeric-id":18274,"id":"Q18274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$EAD85AC3-1F71-466D-A410-17204BFB8A88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f3dc49212bb1ac953b456b7ee6d37c17258b97b9","datavalue":{"value":{"entity-type":"item","numeric-id":18543,"id":"Q18543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$26B9590C-D850-44B3-8079-885908F3681F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"68a02c8b1ab8ed182d6b6b861d09c8de6f71d04c","datavalue":{"value":{"entity-type":"item","numeric-id":21661,"id":"Q21661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$AD790F5B-0F55-4A88-8664-037897563B90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c3aa95a2ec2e1aefe26078e8381cd9d370c279f9","datavalue":{"value":{"entity-type":"item","numeric-id":21663,"id":"Q21663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$6714CAC5-0EA6-494C-91C6-FF5EA544EE54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8820312195fedfa211b44ae20ae12e4a82ec2682","datavalue":{"value":{"entity-type":"item","numeric-id":23299,"id":"Q23299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$39506EA8-4C7F-4FAE-A82A-B460AB625215","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":"Q5170238$47E53B01-03B3-4127-A553-0C8CE50F1310","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3d67782edce6d9e517ef605b890c67d61e3ddfdf","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2012.06.009","type":"string"},"datatype":"url"},"type":"statement","id":"Q5170238$7E54FB5B-D03E-45FB-B951-9C8442231314","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c244cf6965f647b5673aa1a4083cfe4db01e0ced","datavalue":{"value":"W2135156156","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5170238$D2EF63BE-232F-40B3-BE68-E10E799F4698","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"dec0bf3f1f101951654da823516ddbfefffb65b8","datavalue":{"value":"Q113318095","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5170238$A22DEA0D-B182-47B6-9A47-B4FE5D03A052","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c8847fc96bd6cc15667c599e80d53cc2bce3050","datavalue":{"value":{"entity-type":"item","numeric-id":2462635,"id":"Q2462635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$91E31CC5-A0C9-4A73-9DBB-E08E0590E5B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1196f5e17dff99bc1a9d16ec3c58ef966832597d","datavalue":{"value":{"entity-type":"item","numeric-id":2729065,"id":"Q2729065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$9D7834CE-8325-4017-857E-191140C4530E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8910a816017d823e1c2ea267ab4a7baedcd6f69","datavalue":{"value":{"entity-type":"item","numeric-id":5428268,"id":"Q5428268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$CF283BD6-4997-40DF-BD0C-DB762E8F7CA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22686125d766856add6e52adf6a69f059bf713e2","datavalue":{"value":{"entity-type":"item","numeric-id":865648,"id":"Q865648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$5F45C307-32D7-41E0-95D3-D03AF48F1B3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8a4bb921aaa08f7df45e3725952d0cb700416503","datavalue":{"value":{"entity-type":"item","numeric-id":5166497,"id":"Q5166497"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$8D973400-6359-4E4B-9724-65038836B161","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e07a7c2727e1494384a6155100756d5fedce918c","datavalue":{"value":{"entity-type":"item","numeric-id":2867935,"id":"Q2867935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170238$B2C22367-E22E-450B-8B75-BF4E8ADD3A78","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"301dab8e6e81b3fb2dfe89bd64a9b88521173f9c","datavalue":{"value":"10.1016/J.ENTCS.2012.06.009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5170238$603E72D5-FF48-44E7-B5EB-0C5CEB9991B5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9bfe76c583713b55eadf25fa3d88d354ebc06b63","datavalue":{"value":{"entity-type":"item","numeric-id":2879273,"id":"Q2879273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"66f1bd4b32479e0130e8e0642a4bcb8661f6ee75","datavalue":{"value":{"amount":"+0.8598070740699768","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":"Q5170238$6B36E1E6-A44D-4304-B4D9-1C9B979F4913","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e5f08116115338796ec9b797ffb39cc7a493db2f","datavalue":{"value":{"entity-type":"item","numeric-id":2907353,"id":"Q2907353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae0e360a6eb2e1d998ffdb219dadd0524cc7b0ba","datavalue":{"value":{"amount":"+0.8235083818435669","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":"Q5170238$00FB226B-460F-4D5F-B011-C1FBBF0A73AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"353f83759ee34b781b1cadc49c3f90042799760c","datavalue":{"value":{"entity-type":"item","numeric-id":5200122,"id":"Q5200122"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"856bca966b6a700a0ae926d8dd3ec83b0c2808e9","datavalue":{"value":{"amount":"+0.7850741147994995","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":"Q5170238$5AC55958-5E90-4793-9B0A-F0D7DECEEB05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"df287ba4711af7eb66eb6c4530853de65788cc26","datavalue":{"value":{"entity-type":"item","numeric-id":2287890,"id":"Q2287890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5fff4bff7eaed540263549b113241a331aa6120b","datavalue":{"value":{"amount":"+0.7814878225326538","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":"Q5170238$53DC4622-D55D-48C4-AE96-0F8A7E78749F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"434cd42d99560dd27bc63e560daa4f5a831f5dc2","datavalue":{"value":{"entity-type":"item","numeric-id":5166497,"id":"Q5166497"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f4effaa705cdabf736c187aa7c1f939fc8d6ad07","datavalue":{"value":{"amount":"+0.7651729583740234","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":"Q5170238$6CFF54EE-EAD1-415A-932D-8FFBFDAD64BC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5170238","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5170238"}}}}}