{"entities":{"Q6611968":{"pageid":14223125,"ns":120,"title":"Item:Q6611968","lastrevid":42380337,"modified":"2025-06-13T22:53:19Z","type":"item","id":"Q6611968","labels":{"en":{"language":"en","value":"Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7919847"}},"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":"Q6611968$6877419A-1F16-499F-9676-7E4057F92E04","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9fe846497ced4a7dc0b6cb5c8a8a49911d3f6b8b","datavalue":{"value":{"text":"Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6611968$FE7D32CB-84F6-404E-9789-5166ABB619BB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0b5c25c5c15e6cd7738295ea568f4e70d6faf1d0","datavalue":{"value":{"entity-type":"item","numeric-id":6611967,"id":"Q6611967"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$EFBA973C-4F06-42D2-AA0C-471D6028B0CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0c893b180fb25eceb648b78e8f7d155d9dd75e1d","datavalue":{"value":{"entity-type":"item","numeric-id":484924,"id":"Q484924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$8C4DCEAE-6799-4B05-BE09-6A50302973E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3dafc8265e00d5ff0c2def8b15276488609fa8d3","datavalue":{"value":{"entity-type":"item","numeric-id":6168988,"id":"Q6168988"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$2193FAE9-1BA1-4D87-B7C1-F1498C505ACA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$E8EE6476-6F08-4E2A-8344-15B589E75882","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"fa77625b6793398e9785907ea2f3653fa0fbf243","datavalue":{"value":{"time":"+2024-09-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6611968$22DF475B-3F29-43DC-9C27-F0AADF081628","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6611968$EDDB6AD6-9D4A-4A25-A429-B0CF77D6B3C6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fdc56eec44db55e2cbaefa3d78a8f8401c7e12e1","datavalue":{"value":"7919847","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6611968$1B66FE9A-AB9E-488A-A470-680E4A6247E1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8649681bd6e022af57b527d538b7a92c7e6b6e88","datavalue":{"value":"Hoare logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6611968$C84FED2B-2E5D-46FA-8508-E2D7DC266896","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q6611968$DA0ACE75-BC75-425D-AB23-7EA7594ADC6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c1eb112edcb1c678c9102344762b64b2d9359622","datavalue":{"value":"deep embedding","type":"string"},"datatype":"string"},"type":"statement","id":"Q6611968$56D84138-AA40-40D0-8B92-478970C872B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"54ed79f4725dcdad0ab0a3720c5d8bb0d631ff94","datavalue":{"value":"shallow embedding","type":"string"},"datatype":"string"},"type":"statement","id":"Q6611968$13AF0860-C207-4788-9CF9-1A155958B759","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9c89d82b1926316141ae97a9f8fe9f36b24cf27a","datavalue":{"value":"machine-checked proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q6611968$632CFA1B-258C-49B0-866E-63E3282CC172","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6611968$664861F9-964B-4F83-B313-EFD60872C415","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":"Q6611968$283E11BF-01A1-4063-9D27-EAFA09FFC957","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"29a526ec59c544e05de173e8c74ff59db47564fd","datavalue":{"value":{"entity-type":"item","numeric-id":5370885,"id":"Q5370885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$01E1C324-A67E-411D-8391-14724D8E7A20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"138a145b3723972a73dae2c6cdcf8294ccb2b2be","datavalue":{"value":{"entity-type":"item","numeric-id":3000569,"id":"Q3000569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$D683D12B-B8B4-4A9A-866D-5D2D9327F0FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a3f157eb9fb8ce360dd2db17c88b593e185dced","datavalue":{"value":{"entity-type":"item","numeric-id":2649887,"id":"Q2649887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$09656527-1F70-4F38-8ABF-748CC476879F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c061d31b2ad1070c6417d39eb2aecfa3eccd84ae","datavalue":{"value":{"entity-type":"item","numeric-id":879367,"id":"Q879367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$D7C81844-9AC5-4E4D-83BD-F26BEDE29C46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5a1ce762817aa67ba84d34579fd3b9060a2c653","datavalue":{"value":{"entity-type":"item","numeric-id":3543655,"id":"Q3543655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$F74C79F2-7BFF-4313-87A6-33058296305A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"086fdbd21f473c213329b475c94f7dc23f61bf59","datavalue":{"value":{"entity-type":"item","numeric-id":1663238,"id":"Q1663238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$3416390D-66EA-4D8B-AA91-A48298854DA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3343c3ecaf29b3d00ed730793fb135803dd0ca2f","datavalue":{"value":{"entity-type":"item","numeric-id":5176992,"id":"Q5176992"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$FDE3F2CD-7596-46EC-8B8A-30237E093CD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"292d5c006305603ea251952b72b3907af5565470","datavalue":{"value":{"entity-type":"item","numeric-id":5176951,"id":"Q5176951"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$7DF953CE-6A7A-4874-8AF1-B9E0E3B2E542","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"94ee7b1670b832d84e63f3575192ff8a645b95bb","datavalue":{"value":{"entity-type":"item","numeric-id":670699,"id":"Q670699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$A00EADE1-7AC6-4345-ACE4-3756F3103C60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2c71c26bf7e075dc23cee40b3135f1af13e67a2","datavalue":{"value":{"entity-type":"item","numeric-id":4151703,"id":"Q4151703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$6DEF4E8E-0BF4-4C6B-97BA-D99DAA7AD9BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"92ff38abfa4e49dc5b759cba6f43f514f2302692","datavalue":{"value":{"entity-type":"item","numeric-id":5739357,"id":"Q5739357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$C8130D7E-9D12-4574-A32F-CFA1CF05FE75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"567a8dff2d0b10b014f06f4bbf8ecdbec1e09916","datavalue":{"value":{"entity-type":"item","numeric-id":2988660,"id":"Q2988660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$294FD28C-05C4-4EC8-867B-701A9F8EBE12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"95e34163d5f1b6a04f68e439aae1bdd6a4e7e46b","datavalue":{"value":{"entity-type":"item","numeric-id":890377,"id":"Q890377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$2D5917A8-A4E8-4E73-B764-0C743F86529C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc39397aff1a518f386df54d5fcaaed065b005b2","datavalue":{"value":{"entity-type":"item","numeric-id":4625160,"id":"Q4625160"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$27B4B331-3C6F-45E0-8503-73F7798EB474","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9180a995c6bf4fddce09c209e0c80247b0b06901","datavalue":{"value":{"entity-type":"item","numeric-id":2561482,"id":"Q2561482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$991EA8B6-6D43-4BDE-BAAF-DB632A6C87A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f96080269f1ac57df102d277e6fe30615563ee72","datavalue":{"value":{"entity-type":"item","numeric-id":5178765,"id":"Q5178765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$D0BD8037-43FC-4616-A350-72551997D4D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"49fa5b39ffa40b318449c3af5a336d8c38885f30","datavalue":{"value":{"entity-type":"item","numeric-id":3546051,"id":"Q3546051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$0D502775-DBE2-4F46-9E43-C00E482DC054","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"acde0c5acdec560094faaeeaf74535ff9bab476f","datavalue":{"value":{"entity-type":"item","numeric-id":5348933,"id":"Q5348933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$6C230FE4-9C0D-4B48-AA44-E81B93F9290A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$12DB06E1-BE5E-47DA-BCF5-A8BBA1724D73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"17a8c0319a2245226b71de02a8c469bc6287b46b","datavalue":{"value":{"entity-type":"item","numeric-id":3452266,"id":"Q3452266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$69DD7574-9584-4CE9-8D90-605973EF2C2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$093AFD4E-2F17-4C98-935A-18F5D972FCD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18ef9fab9931aeafd0d3a3ca39a098e120e3a610","datavalue":{"value":{"entity-type":"item","numeric-id":3303910,"id":"Q3303910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$918D23EB-D406-4914-B9B7-1F003926FF26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e320d5ab20d9378e83c08a862b63bf2725892d4a","datavalue":{"value":{"entity-type":"item","numeric-id":2653567,"id":"Q2653567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$95D0EFD2-13EF-48FF-8EC0-64B26C1ABD5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"48af5adf09c22725f6f724fe9db0206a76af8fd0","datavalue":{"value":{"entity-type":"item","numeric-id":5464658,"id":"Q5464658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$50128609-2DC6-49D3-B0D0-77086EEBAFB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78204cbee8858331477c8efb0ce846f3c88dd9ce","datavalue":{"value":{"entity-type":"item","numeric-id":5803373,"id":"Q5803373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$C7056494-75FE-4EC0-A70B-145FC31BF871","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ab8803f370a224eac629d99d2c45655ab10934f","datavalue":{"value":{"entity-type":"item","numeric-id":4417905,"id":"Q4417905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$916B5C7D-7378-4357-BF86-2C9DEE22371B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a914c4e44dde41b17e5fb1fd3ebe0fef3dbf648","datavalue":{"value":{"entity-type":"item","numeric-id":2829278,"id":"Q2829278"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611968$42B37D9A-6FBD-43E4-905F-6FCEA2841AEB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"741c0c1036b952ed372b8d45f5b8fa2fe9039cff","datavalue":{"value":"10.1007/S10817-024-09706-5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6611968$CFD0BEEC-12DC-4C91-99AA-A2DAB57B7B97","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6611968","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6611968"}}}}}