{"entities":{"Q2879265":{"pageid":2889985,"ns":120,"title":"Item:Q2879265","lastrevid":52085378,"modified":"2026-01-20T22:02:51Z","type":"item","id":"Q2879265","labels":{"en":{"language":"en","value":"An Isabelle proof method language"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6341494"}},"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":"Q2879265$F70E1C9D-5B7C-43A7-B915-1975C87F39F7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ed9d1c9c4bf7f052faac4af87935bdebcda16c85","datavalue":{"value":{"text":"An Isabelle Proof Method Language","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2879265$C2789EB5-5986-4C9D-BB10-CEDB704E3CB3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0e170819ce2c0a538acaf533ca3d8728c23c425c","datavalue":{"value":"1416.68172","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879265$2EDA63D6-FCAE-48DB-952E-F29B1C50D3B3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"28ca8b8519732adab42099ccbf32ec8855efa05b","datavalue":{"value":"10.1007/978-3-319-08970-6_25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879265$EAB3C8CB-C38D-4D8B-93CF-3682EB4BE1D1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5fbfbec2406713b1ee2886412d7c8dd091cd9c18","datavalue":{"value":{"entity-type":"item","numeric-id":287362,"id":"Q287362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879265$AF760263-2494-45C3-A2E5-01C0733FC928","rank":"normal"},{"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":"Q2879265$4DAC57E9-8C48-4614-A01E-8AC04F1CB15B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"45e6c2a5937a40e685c427c9b959ad4c359ca8cc","datavalue":{"value":{"entity-type":"item","numeric-id":287363,"id":"Q287363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879265$915AF105-A6CA-4A7A-A4F0-A8C153C5BC29","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879265$84BA0464-4E1F-4EC8-B489-D855FED98B7B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"565bc5987614f46e32dc98add32d630fe2eeb533","datavalue":{"value":{"time":"+2014-09-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2879265$EB2E90FD-D3A4-46B4-8DBC-498DA3E648DF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879265$5558339D-B9AE-497F-AD0E-EFD539907CF6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ea48ccbf86878b9c3c7659a235d63f4d7458df21","datavalue":{"value":"6341494","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879265$A7F1F550-06B5-48D3-98E7-EE3B9AB04BAA","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":"Q2879265$988C2023-AFFD-46A4-891E-787CA999C03C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcaf3b20cd7fd897f2f47a708bad9d4f554cb6fa","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879265$7F05FCB8-D39B-4A5A-9FB7-752402B63ACA","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":"Q2879265$1C197C05-B4E4-4D82-B703-167844EC10EE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2a7155655ef2822c08e5bf3cf7595d8d46393bcd","datavalue":{"value":"https://doi.org/10.1007/978-3-319-08970-6_25","type":"string"},"datatype":"url"},"type":"statement","id":"Q2879265$95F72688-FF10-42A8-9BC0-6C2A3207C25D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a89121618f2371579c3ee3f46e842bd640dd73c7","datavalue":{"value":"W315511896","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879265$C19DFF12-0CB2-4E54-BAE9-52C0B98BD028","rank":"normal"}],"P1643":[{"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":"6af58e23340e9faf85fcf2454ada165d45ac994d","datavalue":{"value":{"amount":"+0.9819318652153016","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":"Q2879265$DD4608DC-2F04-4399-957D-BE1F166CC2D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c1fbe8f76631e9b24e2621b72c3ad8cc01fc1fd0","datavalue":{"value":{"entity-type":"item","numeric-id":1868515,"id":"Q1868515"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"439990755f9ce2cdf2c05750754f3457da587682","datavalue":{"value":{"amount":"+0.7557729482650757","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":"Q2879265$8B318686-5D76-41B6-B1D0-AFE782EA0614","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":"e2c28e40efb9cfa1320060bc32b9e373bdb4852f","datavalue":{"value":{"amount":"+0.7531517744064331","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":"Q2879265$970207AE-5531-4981-902B-9D17875A7854","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":"7fc7154f788592ce0bca4b4bad57185d7803b641","datavalue":{"value":{"amount":"+0.7531487941741943","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":"Q2879265$FABA59E7-4079-41F9-9786-AA2233498BC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ef914c5d16ae991870856bd539a5283395a477b7","datavalue":{"value":{"entity-type":"item","numeric-id":3543647,"id":"Q3543647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d1bc72dec120453bb4e65b49a0e433ad5bd4727e","datavalue":{"value":{"amount":"+0.7527742981910706","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":"Q2879265$A45AC64E-CFB1-41DC-A26A-CF5DC8EFC53F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2879265","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2879265"}}}}}