{"entities":{"Q3452263":{"pageid":5227924,"ns":120,"title":"Item:Q3452263","lastrevid":52391840,"modified":"2026-01-22T13:10:51Z","type":"item","id":"Q3452263","labels":{"en":{"language":"en","value":"Abstractions from proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6507270"}},"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":"Q3452263$24782D0B-8503-497A-8699-5BE762E50E41","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a2ad4e2c58434cb9dd6f85f49531e2ca6068aaaf","datavalue":{"value":{"text":"Abstractions from proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3452263$EA1F7C31-0B90-41D0-825F-79042FDD2924","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"58c0e67fa7fd4533817a180a3e2cb1d7740b41f2","datavalue":{"value":"1325.68147","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3452263$B5E4D34E-2D61-4BF4-B38C-25637ED2295A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"660ec4dd32d3eb501abd2f14aa7be4ddf324d8a4","datavalue":{"value":"10.1145/964001.964021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3452263$204B23C3-DE04-4DA7-8B53-DCAD6FA5CD23","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2109ea3ab29767c79eca725b68331d0c21a9a6f0","datavalue":{"value":{"entity-type":"item","numeric-id":2225085,"id":"Q2225085"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3452263$97AAA544-BF37-4AE3-AE67-F69F26F5C72D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cd27e91c4471a6c2f2d14ef8212c1a71ddfcbbaf","datavalue":{"value":{"entity-type":"item","numeric-id":453531,"id":"Q453531"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3452263$1A07EEE7-67D2-4DCE-9C3E-BE8BC2EEE4AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"57a84b3343ed70002617a9eb1439c18c15bac9ff","datavalue":{"value":{"entity-type":"item","numeric-id":934708,"id":"Q934708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3452263$FFB16112-A40C-4B12-8C1C-7475E4ED9B97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e91931f3fd780c36ea4328f78b3c3352f7c16650","datavalue":{"value":{"entity-type":"item","numeric-id":355505,"id":"Q355505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3452263$9F8BDE7E-9DEE-4C5C-951F-9EC4DB367AB7","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0852588251a756a8ac86204eccc7b587f97246ef","datavalue":{"value":{"entity-type":"item","numeric-id":3452244,"id":"Q3452244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3452263$837C9AF0-B6B7-40AD-A9B7-C3AD98BA3637","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c539994eb381dc1a629fdee36492e4b7f4d8928a","datavalue":{"value":{"time":"+2015-11-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3452263$C1079FC0-3587-44D0-B6CB-FDEC9A9BFC52","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3452263$F80657CD-3FB9-4525-B43A-E7C70EDA9F2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3452263$327A0E27-D06F-4A68-8A8C-CF5495290ACC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"be1233dc9aeaccbf4dad7f605ce3b27f85e78166","datavalue":{"value":"6507270","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3452263$097FC331-6AF0-4DF0-8DEA-FC67DF2A4DCD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4d30b34df7da5166d77be8c10d1d4558f1f1fb29","datavalue":{"value":"counterexample analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q3452263$7765A96C-371E-476F-8F6A-9EE9BFE73843","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c9fb50508d9ae1a4b5b2525656ffbf4223c07463","datavalue":{"value":"predicate abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q3452263$32C55D4C-12B2-4421-BF63-E032EE8D05D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c0e3f8f91d1559da40b3e6abc73d4e0baa9c0808","datavalue":{"value":"software model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q3452263$D54F179D-BCE4-4C00-992B-D723238076C8","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":"Q3452263$33EA0434-B93C-4C4C-9832-31A47655A5B1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fcc8e7181e144c2b1a3ff602d715c6c28f310446","datavalue":{"value":"https://doi.org/10.1145/964001.964021","type":"string"},"datatype":"url"},"type":"statement","id":"Q3452263$8A9D27CA-ED16-428D-996E-96AF9F61582C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e6f6cd452aaf60ae483882d9d41763f48ba4132f","datavalue":{"value":"W4212792638","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3452263$8502D01D-588C-4469-87FA-E9BC4F461DCB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb253fb55714f511287e3fb7db3bf54cfc2f7066","datavalue":{"value":{"entity-type":"item","numeric-id":5311270,"id":"Q5311270"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5c0621f824255b8a7909c338b494f4bac392b0d9","datavalue":{"value":{"amount":"+0.8502811193466187","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":"Q3452263$70C11EBD-872D-4ADF-B18B-5B94D62D7082","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"35471693b9b81aca4d54d85b5e7a7d84e4829dbd","datavalue":{"value":{"entity-type":"item","numeric-id":5756749,"id":"Q5756749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6e283d77672b31a535bfb8cf43f98d4cc71c42d9","datavalue":{"value":{"amount":"+0.8454573750495911","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":"Q3452263$7A4A172B-16C7-4EF7-9A18-BA9210157862","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"609db31109f29daf5f20500cb6e669dae387d5e6","datavalue":{"value":{"entity-type":"item","numeric-id":5902361,"id":"Q5902361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c27df42ca14b6b0f1143c6f1ab01ca1bfc2fa235","datavalue":{"value":{"amount":"+0.8421918153762817","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":"Q3452263$AF9F52CF-43E5-4084-B6CF-BCF8B56F8E95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9312a021d07435c43a4923db960b9c16ffaa086e","datavalue":{"value":{"entity-type":"item","numeric-id":3620428,"id":"Q3620428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5987a20219ae3508ed76219f6b786206b558e744","datavalue":{"value":{"amount":"+0.8329841494560242","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":"Q3452263$C77E4751-1C77-4FBA-B352-64CBE6ACE9E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d7b7a8c6f01dfecc18f5236dd4a0db19a4b41985","datavalue":{"value":{"entity-type":"item","numeric-id":5899075,"id":"Q5899075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0f812da9576340b092ce305b676fe4053eee9b8d","datavalue":{"value":{"amount":"+0.8194540739059448","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":"Q3452263$35E88EF4-BDEB-4089-BECC-ADEDD0779734","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3452263","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3452263"}}}}}