{"entities":{"Q2405272":{"pageid":2416015,"ns":120,"title":"Item:Q2405272","lastrevid":57899415,"modified":"2026-04-03T00:25:46Z","type":"item","id":"Q2405272","labels":{"en":{"language":"en","value":"A proof strategy language and proof script generation for Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6778424"}},"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":"Q2405272$0322A386-364A-4536-8C2E-29C78ED13068","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d0ea9f25911def2e360d2b5ae8ee8c2a52cda42a","datavalue":{"value":{"text":"A proof strategy language and proof script generation for Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2405272$92A99042-EA51-41BC-9995-C1448CB8714E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d6194d2ed4c9d623894fccb9bc6785cb245f09e9","datavalue":{"value":"1494.68290","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2405272$65A36823-268A-49A5-9F6D-4BBBF77B8F15","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"dedd43fe1597767e472717b5d08de8fa7976e133","datavalue":{"value":"10.1007/978-3-319-63046-5_32","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2405272$65F6344C-AB20-476A-9FEB-7D2B6B461A2A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bad250d2383a6addb9f20421ad8f0febdd8925ab","datavalue":{"value":{"entity-type":"item","numeric-id":1798970,"id":"Q1798970"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2405272$B9F4A7C3-C725-4019-BBDF-48135137FD35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"62025305e3524f61b1fc8b1f7bbd2484241846ea","datavalue":{"value":{"entity-type":"item","numeric-id":287359,"id":"Q287359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2405272$3039FC13-5453-4960-99E9-3D64279DAE39","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"75b8eddfcc302defc1a614ef0ded8c7b941f1ef4","datavalue":{"value":{"time":"+2017-09-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":"Q2405272$37E6C92B-0121-4FFB-8257-505258578C4C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"073aa4d7f3a0a73728f53bf25aedb028800ec003","datavalue":{"value":"https://arxiv.org/abs/1606.02941","type":"string"},"datatype":"url"},"type":"statement","id":"Q2405272$1A578E73-6B11-4A19-ABBF-E7B0C429C99D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2405272$35A4ED50-4339-415C-84E7-1D777721BC8B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bc3e57718f571ae1fc112e44dfa818d4e9a07e69","datavalue":{"value":"6778424","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2405272$CD41D55D-1ADE-4174-85FF-86F31ACC069D","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab1ccc8faeab7e6c417af9846c477f0e521ebe1b","datavalue":{"value":{"entity-type":"item","numeric-id":14592,"id":"Q14592"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2405272$F2C3FDA4-5109-4521-B15E-8886F82319C9","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":"Q2405272$5032A5D4-2026-45D4-934F-74239B208778","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":"Q2405272$9C820B10-B63E-4B78-B416-611EB86CC7A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2405272$9795AA66-DF0F-4A17-9286-0DAB261BC4B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"39d1d25ae8c00cfad058b188db36fd61dac09925","datavalue":{"value":{"entity-type":"item","numeric-id":27041,"id":"Q27041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2405272$1B2841F1-51DE-4D24-95A6-097FFDC0E6A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9b0860d94af5fdff4b5635709ae334aacdf07ca1","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2405272$6954026F-12B5-4CB9-BADE-60BC08F89B81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6c7e65d45048f1659040b4ae3ed77d872ceb74e5","datavalue":{"value":{"entity-type":"item","numeric-id":33390,"id":"Q33390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2405272$6F9EF350-D9BF-47E4-B371-7CE27C8E2DF5","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":"Q2405272$ED77E3DF-AA9F-4E20-9B20-414ADBCC68F0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a064673e2642733e9e0e558ae9ea2c9772d05a50","datavalue":{"value":"W2962820807","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2405272$FAA42989-DA8E-4A2A-BF89-439BE97AE201","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9374931cf68530b34205f633bba9ad4c29b915d8","datavalue":{"value":{"entity-type":"item","numeric-id":2870138,"id":"Q2870138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a7c04359ba49df1673ac1b097382f4b971a3767","datavalue":{"value":{"amount":"+0.7713148593902588","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":"Q2405272$C9C7B5A1-B920-4427-A3F8-8390D341E3C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5f94645fe7f1525963701159b1c6851e22f8eef0","datavalue":{"value":{"entity-type":"item","numeric-id":287340,"id":"Q287340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a877d45db20b23aefb90c56ae38280049fd4cad8","datavalue":{"value":{"amount":"+0.7656237483024597","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":"Q2405272$0224B474-CFB0-4D8E-AD0A-9C72FD507810","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a94ba17c125ab4086b43d15a4f8cd877edee070e","datavalue":{"value":{"entity-type":"item","numeric-id":1798971,"id":"Q1798971"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"42122343b15b29893219f6d2654dad11651d4402","datavalue":{"value":{"amount":"+0.7640571594238281","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":"Q2405272$428A3098-01BE-4583-8BC2-5C1B4C0FD86F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"920441f7c620bcab29bf4b5663cc031d0c1265fc","datavalue":{"value":{"entity-type":"item","numeric-id":287365,"id":"Q287365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4fd38659cbb160b700845be4d250f9fcf1dda903","datavalue":{"value":{"amount":"+0.7554336786270142","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":"Q2405272$176A7D57-FE66-40C6-83B9-A4BE39A3BFDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38394b4e8d3a3502630a463829cd1f4840ac5524","datavalue":{"value":{"entity-type":"item","numeric-id":3172879,"id":"Q3172879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9369eac0296b3da33305fcf759f5374c43e92405","datavalue":{"value":{"amount":"+0.7515208125114441","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":"Q2405272$B6906F6F-C891-4D20-A1E4-1CAA92B48BCC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2405272","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2405272"}}}}}