{"entities":{"Q3334054":{"pageid":3344762,"ns":120,"title":"Item:Q3334054","lastrevid":48728236,"modified":"2026-01-05T17:43:21Z","type":"item","id":"Q3334054","labels":{"en":{"language":"en","value":"Mechanical proofs about computer programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3866559"}},"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":"Q3334054$228EF9AE-4804-421B-99BB-B777F3356C3C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"362263e76679d4e9475320805c0a204e048e20cc","datavalue":{"value":{"text":"Mechanical proofs about computer programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3334054$50E5536F-8801-4474-BCD2-4F9B2D498C40","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"27888310ecd07bb3fb51cd261a7d85e342f44770","datavalue":{"value":"0544.68012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3334054$697D2B6B-3E5A-494E-B63D-BD4862012D96","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"53805896e3ca7ab179f5f6fd127835e9a6963626","datavalue":{"value":{"entity-type":"item","numeric-id":3334053,"id":"Q3334053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3334054$7273770C-6DA7-47CD-BC01-2BBFF9E93B37","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e136bbdda99981f780084921153c27ffb0ef7a8b","datavalue":{"value":{"entity-type":"item","numeric-id":3028582,"id":"Q3028582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3334054$EC05D8A8-435C-48E0-975F-F9E38D728E05","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ee0f220147ae8bc749a64db56839865dbc4f127","datavalue":{"value":{"time":"+1984-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3334054$C2DCFF0E-5018-40B7-B9E1-6FC6DF2FBDA1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3334054$B36D785E-9686-48DF-8A83-C1A8C0994928","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"517ace4a4f9c45a5475b4a8927a567447dbdb293","datavalue":{"value":"68N99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3334054$CF953125-2C5E-43F4-901F-58A9B974661C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5fbed11f067e5ce7fb5e2e1f69f2f4a7df52d1c6","datavalue":{"value":"3866559","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3334054$D82104E5-9B33-4C7F-BFBF-0079EE88FC1A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb49467b0eaac11205bea2d762375c665f5d0a6b","datavalue":{"value":"software engineering","type":"string"},"datatype":"string"},"type":"statement","id":"Q3334054$93E13958-4CD2-4BE3-AB04-F9CB4D80B79E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"323c5fab6f2e2623caad970a1b112ff710cf1523","datavalue":{"value":"Gypsy verification environment","type":"string"},"datatype":"string"},"type":"statement","id":"Q3334054$2EBAE2EA-74ED-4F6A-867D-667CA5E0005B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c288c642b0c4101c3cf7c676a7ade36e5b404861","datavalue":{"value":"specifications","type":"string"},"datatype":"string"},"type":"statement","id":"Q3334054$35034917-13EC-49B9-B921-8EF972AA5678","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"928e5c514c241b2646f93d7e4af2a1b759902382","datavalue":{"value":"mechanical proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q3334054$5C882F6D-17F9-4DA1-9435-CE12BAC64696","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5004d80ca42dc86b0d724acccae2d60ec857b96c","datavalue":{"value":"Gypsy system","type":"string"},"datatype":"string"},"type":"statement","id":"Q3334054$01108FA0-89FF-406F-BBE1-7D4CD657D286","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":"Q3334054$E268ABF7-E40A-4FF4-9BB6-F7022C6115B9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cb0df05dadf487458bf22613e261fdec228b6064","datavalue":{"value":"https://doi.org/10.1098/rsta.1984.0066","type":"string"},"datatype":"url"},"type":"statement","id":"Q3334054$A1B67522-E86F-482B-A641-14F0CD5F74FF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e104759312310d0a5ce1c87b382381ac5622bb80","datavalue":{"value":"W2170606394","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3334054$8D297067-76D2-4725-9DD8-D2BBC5FF1027","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"574f4bb84f2ae0e95fe9d15b8f43f525aa395e42","datavalue":{"value":"10.1098/RSTA.1984.0066","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3334054$8D39033A-0811-4F5F-8C87-35966CEC711F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cdf843fc562649d5f1d6e00070732b576086513d","datavalue":{"value":{"entity-type":"item","numeric-id":3654815,"id":"Q3654815"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"27d12f27645450b75665e431e0988cebd4f734a7","datavalue":{"value":{"amount":"+0.7441520690917969","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":"Q3334054$59DCF43E-02C9-462D-B312-7B1387021AD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"286621dceae39ed4c4865eaae2eefab2f27b11b1","datavalue":{"value":{"entity-type":"item","numeric-id":1316958,"id":"Q1316958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3f6ce7205acb31e482424a1d2d5ead1dc033c43d","datavalue":{"value":{"amount":"+0.7390291094779968","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":"Q3334054$779C416C-B206-445A-8C78-A40F8B2B536A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"019a14f51c461e45f89e4801a279c3e28305f2c6","datavalue":{"value":{"entity-type":"item","numeric-id":1419888,"id":"Q1419888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3f6ce7205acb31e482424a1d2d5ead1dc033c43d","datavalue":{"value":{"amount":"+0.7390291094779968","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":"Q3334054$33FF11D1-F729-4556-9F42-3F2D3AB087CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"678c0c38f6268df2cba63533bb44a641d219e574","datavalue":{"value":{"entity-type":"item","numeric-id":3197301,"id":"Q3197301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"03a0c679768acb6a3dab6c282e24d10d0e9e2e4d","datavalue":{"value":{"amount":"+0.7351061105728149","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":"Q3334054$2F2428D6-0C94-4D69-8883-C35800E37CD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"704cd94a73c558bdd650432d127140d969aa817a","datavalue":{"value":{"entity-type":"item","numeric-id":3326818,"id":"Q3326818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5f12ff4ff70e37c467e0a303ee92df5fb05ea161","datavalue":{"value":{"amount":"+0.724780797958374","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":"Q3334054$11175A69-464E-446B-9FC4-84C2CCA01AA1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3334054","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3334054"}}}}}