{"entities":{"Q2281658":{"pageid":2292401,"ns":120,"title":"Item:Q2281658","lastrevid":57819810,"modified":"2026-04-02T16:21:11Z","type":"item","id":"Q2281658","labels":{"en":{"language":"en","value":"Automated mutual explicit induction proof in separation logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7147588"}},"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":"Q2281658$C7844FF1-A9B1-4325-8A9A-7D6066830F5E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"afae9753df5c7833d1a67881b4108caa21e403ec","datavalue":{"value":{"text":"Automated mutual explicit induction proof in separation logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2281658$00C1F48C-3327-4B07-A669-3B9CC492BD93","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2d48057c6b3060537e584bdb7ba1248c4ad568d2","datavalue":{"value":"1427.68350","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2281658$D10442FC-2D6A-4319-8271-2C2C04AE76BE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7a31387a7bbf61d3c42b9ed61beaf82a28265d08","datavalue":{"value":"10.1007/978-3-319-48989-6_40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2281658$8FDF62C3-9A4B-40F9-91A7-5E0FD8F084FB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"109e9485d12cb8a1aec75d16072ef10f0c2e11ef","datavalue":{"value":{"entity-type":"item","numeric-id":2234086,"id":"Q2234086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2281658$EF43A4A0-6EDE-4147-908A-616DD61B74B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f7d65495ab5558ff62ea59fe4039592e5464f999","datavalue":{"value":{"entity-type":"item","numeric-id":2281657,"id":"Q2281657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2281658$2C90AE33-9BC1-40A5-94F7-417DC5E3E63B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a3ee23cd67d40d34f50126c9eae32be36f4578c5","datavalue":{"value":{"entity-type":"item","numeric-id":238509,"id":"Q238509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2281658$1291D8F2-4C11-48F1-9D31-4FC658A84A85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7350aed0b0267db3934820cd5357095f0cb6b7b1","datavalue":{"value":{"entity-type":"item","numeric-id":238508,"id":"Q238508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2281658$44CAAE78-4D00-428E-BB06-5ACA013B368A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f19ec05f4cc07189117a4725b428f63f5643b194","datavalue":{"value":{"time":"+2020-01-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2281658$773D489B-9811-410A-BE88-3F8803006325","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"744a04118f26e9d69133bdfa971a2550e2b1efef","datavalue":{"value":"https://arxiv.org/abs/1609.00919","type":"string"},"datatype":"url"},"type":"statement","id":"Q2281658$2A7AEC39-B7E7-4856-8C86-969A40F74DC4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2281658$64A1D6AE-0E5C-44CF-B83D-45D0D56C6156","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2281658$0A9109B1-C7F5-4606-BB03-1003ED195E22","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bb57224b674ed3416aa5f20a4b893a579b73ae20","datavalue":{"value":"7147588","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2281658$78E59BEA-C3CF-4D03-A1FD-FFB0F3FF3DD0","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c71db78c9c0301319342ea53aa84a13ff5995264","datavalue":{"value":{"entity-type":"item","numeric-id":44082,"id":"Q44082"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2281658$3A9943D8-E330-4B43-86AC-12F63B88C371","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2281658$C9B2148D-DD21-420C-9923-2870BC33D6EB","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":"Q2281658$72D2F73F-D1B2-4AE2-B3FA-25D264DBAD3E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1b0fee502616e1ebe5c76e3b759330de00eaa9a9","datavalue":{"value":"W2512685755","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2281658$E1659635-EFD5-4ED6-A22C-DE39C4ABB53D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"951890c12966d7711b57fa25199ae479f8514306","datavalue":{"value":{"entity-type":"item","numeric-id":2414251,"id":"Q2414251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1d4fd34bebf56c084633b12863a2b297db00ffc9","datavalue":{"value":{"amount":"+0.9694989919662476","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":"Q2281658$D9BE70C4-39ED-4AAF-9C88-1666D3779026","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8ce9665b91ecb3a2eb7e60be16e012a2320e66e4","datavalue":{"value":{"entity-type":"item","numeric-id":5200020,"id":"Q5200020"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"54cd1834026e83091817747b2fdd46a6e3801c79","datavalue":{"value":{"amount":"+0.826164186000824","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":"Q2281658$CD050A46-4407-4428-A52F-FC66BC632962","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a0eecc6dbf75532216f5e876fe937e096817d861","datavalue":{"value":{"entity-type":"item","numeric-id":2324205,"id":"Q2324205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c1249b99cbf8b41c1c86b4add7b17bae87f36203","datavalue":{"value":{"amount":"+0.7776790261268616","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":"Q2281658$3A520EDD-C999-4F21-AE1E-C281D6E687B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7c1694d6bf440cb2a8ed659587389564d3cae23a","datavalue":{"value":{"entity-type":"item","numeric-id":3454118,"id":"Q3454118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4e441b1dad11966f8d22a4fe6b624055ff2517c8","datavalue":{"value":{"amount":"+0.7589917778968811","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":"Q2281658$477CA076-D19B-47DF-BE90-1DAE466C59B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4e19bbb791608ca63a345b3983f727d0d9a2b56","datavalue":{"value":{"entity-type":"item","numeric-id":3457790,"id":"Q3457790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"682b17cc3ff0e8cf15f55e893965fac437ad7ec3","datavalue":{"value":{"amount":"+0.7564817667007446","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":"Q2281658$DD92951A-B7E0-4457-839D-94AF49B8D825","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2281658","badges":[]}}}}}