{"entities":{"Q2848061":{"pageid":2858781,"ns":120,"title":"Item:Q2848061","lastrevid":51832673,"modified":"2026-01-20T06:37:17Z","type":"item","id":"Q2848061","labels":{"en":{"language":"en","value":"Bounded model generation for Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6211415"}},"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":"Q2848061$F1D884AA-348D-43AC-B976-54DDE609D8C3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"53bb84387c95c04c00c28aefe0a5a8e8a77935d5","datavalue":{"value":"1272.68365","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2848061$E764C83E-4B15-4C38-A8EE-5894E905413F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d1f8cd3b806fd78547b3f4844ba487e41a5ec455","datavalue":{"value":{"entity-type":"item","numeric-id":286783,"id":"Q286783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2848061$6BDC8957-A72E-47AE-9F45-6C792F8028B6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"68e9606d4f4e53be9a37b58bd23167a8b2b94aea","datavalue":{"value":{"time":"+2013-09-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2848061$63F6746F-3982-4EF8-B495-90F5E9405C33","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b173b40db195fd0dc7e3785e85a637edae8a8144","datavalue":{"value":"http://www.sciencedirect.com/science/article/pii/S1571066105050759","type":"string"},"datatype":"url"},"type":"statement","id":"Q2848061$74F8C9A2-B72B-4E59-88B9-2A0CC5A67785","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2848061$0223446A-1A19-4257-85D3-DAC10E03BAC9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3ff0cfa59dfa6c489f1a96f31e364139d7e00cf0","datavalue":{"value":"6211415","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2848061$1A7CF31C-B25D-4CD3-B30D-42268E81C80F","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":"Q2848061$48E28B93-8E07-4933-8438-C650D681EB28","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":"Q2848061$C61117F9-0A9C-4D43-B581-D36ADF2433EE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f4070c6470d49a4f33f299f221281240fab674ee","datavalue":{"value":{"text":"Bounded model generation for Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2848061$1FD06825-475F-4EB6-9E65-13715896CEE7","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0deab03664bb05ee0ab93f02e3e2aa8174c99308","datavalue":{"value":{"entity-type":"item","numeric-id":5747646,"id":"Q5747646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"de923e9e42d657ea4d75ab93b9ac086625a736b8","datavalue":{"value":{"amount":"+0.7962791919708252","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":"Q2848061$117D6685-5BA0-48CC-B37F-52880A9838C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c9a6d991b50ee3cacf0f632a65fb75701662b114","datavalue":{"value":{"entity-type":"item","numeric-id":2405244,"id":"Q2405244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f7af04a15fc0546addbdb92828e13256268d5bfe","datavalue":{"value":{"amount":"+0.7805935144424438","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":"Q2848061$CEB10DF8-0FAA-44E2-87B2-BB44B062D242","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":"44829d88aca0561a531b3c93642498869722a0f6","datavalue":{"value":{"amount":"+0.7514366507530212","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":"Q2848061$88EB413B-9172-4809-AB79-518E532D12D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6ef4d4de289000e0b726d89ac0d7d5d3c7e3196c","datavalue":{"value":{"entity-type":"item","numeric-id":5698259,"id":"Q5698259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8758ecd754f8cdd9b6940c25d9c5035a4398c0f6","datavalue":{"value":{"amount":"+0.7440086603164673","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":"Q2848061$49C6FF39-E088-4EBE-9904-3912C84BD9FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0880741c3c12b53e29e3e6a1d6dce99a7cfef870","datavalue":{"value":{"entity-type":"item","numeric-id":5200021,"id":"Q5200021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56765d0152b95605a6ae32170e8becd37e3879bd","datavalue":{"value":{"amount":"+0.7224477529525757","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":"Q2848061$8502712C-6655-4843-A93D-A5F8BC9DD74A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2848061","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2848061"}}}}}