{"entities":{"Q3060983":{"pageid":3071699,"ns":120,"title":"Item:Q3060983","lastrevid":86095640,"modified":"2026-06-03T14:16:44Z","type":"item","id":"Q3060983","labels":{"en":{"language":"en","value":"Mechanized semantics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5825967"}},"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":"Q3060983$E0D002F5-26E9-465C-A926-93F301E1DD30","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dd17d4428813b9a16867eb6e60dc6e44ad85da47","datavalue":{"value":"1213.68206","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3060983$B6000E79-CC60-4760-8B56-16D3E1CDC373","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1ccc73339958bfa4b01570a7aced0ccc270bd336","datavalue":{"value":"10.3233/978-1-60750-100-8-195","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3060983$35F02814-A384-4BBC-B5BB-0C079204B4C7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c4b1e35c1c4bff0a8e8e775e8600e2e952b118ae","datavalue":{"value":{"entity-type":"item","numeric-id":848738,"id":"Q848738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3060983$5F9A6713-02F6-4183-AF70-DAEB1B013F3B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1a148a0f7f88b9e1cbbef4b920e7c605d6b8ccf5","datavalue":{"value":{"time":"+2010-12-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3060983$AFA6245F-729C-4D69-9741-EE29104F366C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2300239016a8c3f851966cd114148fa268cbbae5","datavalue":{"value":"https://arxiv.org/abs/1010.5582","type":"string"},"datatype":"url"},"type":"statement","id":"Q3060983$260DD33B-AEFC-4D07-9906-D90C821C9981","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3060983$D9C16CC5-CC29-462B-93C1-315E3BE1B70A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3affb2aa66be15f2a63c60d2aaa92bd143e6d46","datavalue":{"value":"68N20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3060983$CC9F34BF-189A-428F-A2F3-032BFD1F29EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3060983$0CBB933A-A03A-419C-B85C-0681B0A4735F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3060983$47B18F6C-6BAB-4E30-A752-277F79608C0D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3c142c77e1393fe10a3a5fd7c176352dd9c90327","datavalue":{"value":"5825967","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3060983$7F26A363-C10C-4654-B776-189F554E7BF6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"98456cd4cdf0db037b678749018452921ff9260b","datavalue":{"value":"Coq proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q3060983$028F35F3-A374-44D4-ADFE-C85B42E925D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d15a5b88457b15e43f49d0900c124a1c1adc72df","datavalue":{"value":"operational semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q3060983$AB71FF07-2932-425D-AF17-6B38F020E27B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"51802126f63d5102d578f2858428d5d0f09da73b","datavalue":{"value":"denotational semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q3060983$AA17B028-838F-4F1A-93DA-61A72E16C3FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c078ac6b4aa6494d6d5c36981e624a189730ba5a","datavalue":{"value":"axiomatic semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q3060983$96A73CFD-88BB-4BA0-BCD9-8CC17D26AB5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8649681bd6e022af57b527d538b7a92c7e6b6e88","datavalue":{"value":"Hoare logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q3060983$065E61CB-E31B-49BE-B7C6-A083BCA04535","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6c9625802d2a4af150754fe4445b660a88ae6a79","datavalue":{"value":"generation of verification conditions","type":"string"},"datatype":"string"},"type":"statement","id":"Q3060983$B2484E0C-F213-46A1-BDA5-2747A7F36939","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3060983$45ED0B47-8939-40BB-8AA9-FE8CD01A43DE","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":"Q3060983$615FE0B4-0D9E-49C7-A817-CF530DE1BBCB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3a5818217002846097fcdd505c0d40e9a8ce953d","datavalue":{"value":"W3037420009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3060983$D3189DDB-DAC4-4888-AB0D-C84005B0F41F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ca34a15b1a9976d94868e7904aaa581c2d9d62d0","datavalue":{"value":{"text":"Mechanized semantics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3060983$259EE50D-23EF-475F-8421-7271384D25A5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a81a6e0ee5b47b893ac70653e844d8160c093751","datavalue":{"value":{"entity-type":"item","numeric-id":2761214,"id":"Q2761214"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"17fc911eae438bd62e484048181b82d031023ccf","datavalue":{"value":{"amount":"+0.89767927","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3060983$B187D9B3-C12F-4AF8-993F-409C2096ED50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"653bb42b19be8ce2e8f831ce06cf512b9e69994f","datavalue":{"value":{"entity-type":"item","numeric-id":5311261,"id":"Q5311261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6d39f5dee10e4b1a44363753a4e31418f733760e","datavalue":{"value":{"amount":"+0.8968835","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3060983$6634AF31-144B-4B30-A6CE-8018466B935C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ed58649527b45a30c8bf0f209a9b2229e7451a53","datavalue":{"value":{"entity-type":"item","numeric-id":1267030,"id":"Q1267030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cf3e74413047de60e6d8cdf44d322c0f2c37eca7","datavalue":{"value":{"amount":"+0.896554","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3060983$4C2A03C7-FE6D-4294-81DC-EA43F10FBE2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"17175b224c7515c72d73abe77c54bb3cf1b4320a","datavalue":{"value":{"entity-type":"item","numeric-id":4916051,"id":"Q4916051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"700d09598bf204a9d9b4cd11e941ebecd8449e18","datavalue":{"value":{"amount":"+0.8963332","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3060983$E3E5D6F9-B257-41EF-96A4-CB47E1DFDED4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"608620170593ad619f06b2819a60970a671696ff","datavalue":{"value":{"entity-type":"item","numeric-id":4471724,"id":"Q4471724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5858a1e49b127c76d72c162950d6bd876e9c3eae","datavalue":{"value":{"amount":"+0.88570565","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3060983$6DD572A0-3D1A-4622-82FB-1FD0CD4770FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1551005f43c7e0066c57228be407a1a60893fbf9","datavalue":{"value":{"entity-type":"item","numeric-id":5402521,"id":"Q5402521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c0b097ec790a104a0e0bc60f5c274c7c01c9dcc5","datavalue":{"value":{"amount":"+0.8839089","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3060983$CE3B964D-71D4-4342-8C6A-43FB93777CF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"150ec41cca31534b83a2031a23ff46f22a466d9e","datavalue":{"value":{"entity-type":"item","numeric-id":2945730,"id":"Q2945730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7b5837c45bd62b5a0cb86ae046b9195223b436ba","datavalue":{"value":{"amount":"+0.88178456","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3060983$1630FF7E-3134-4572-B2DF-135D430E532A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mechanized semantics","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Mechanized_semantics"}}}}}