{"entities":{"Q2942880":{"pageid":2953600,"ns":120,"title":"Item:Q2942880","lastrevid":52343366,"modified":"2026-01-22T09:45:29Z","type":"item","id":"Q2942880","labels":{"en":{"language":"en","value":"Static and user-extensible proof checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6481254"}},"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":"Q2942880$20592BE1-F49F-4DEF-ACA0-845EBD9D1C16","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"44acef1ddcf503a2668c355270e6f5294563f7e9","datavalue":{"value":{"text":"Static and user-extensible proof checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2942880$1E54DAB8-1ED5-4BEF-A74D-0785742CAD91","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9e6f7c514e6f38006503da4cdf417240186e7d76","datavalue":{"value":"1321.68204","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2942880$F25A0827-2C66-4764-BAAD-B441A9BC6241","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e06de17f813cf52dbc7714a83d4a5c9e27b6826a","datavalue":{"value":"10.1145/2103656.2103690","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2942880$A84D1AFD-27DD-4E35-B28A-8598918A976B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"dd83bd74c907c998e088268ecc586b95f425c756","datavalue":{"value":{"entity-type":"item","numeric-id":2942879,"id":"Q2942879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2942880$08983667-A9D2-48E5-866A-361DB4BD027F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b45204622bfa7b343b3d270acbf7de72b0faad61","datavalue":{"value":{"entity-type":"item","numeric-id":835763,"id":"Q835763"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2942880$143202AD-D841-42F9-9C84-1E7B757B5829","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b2e3947a47402cf435bd22e833e203adf92b612a","datavalue":{"value":{"entity-type":"item","numeric-id":2942852,"id":"Q2942852"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2942880$D803C209-363B-4A0B-A68D-4A3F104B27ED","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4dc3af13f56c9757ccde8db0e7a8779bcfa3e4e2","datavalue":{"value":{"time":"+2015-09-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":"Q2942880$A2751D84-810C-4C0C-BD88-A34F0DEC31C2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2942880$984403B8-47CF-4A46-A419-BC26E930D011","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2942880$03F6E689-CD00-419F-974C-B6FD3EF4D708","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2942880$6E81CB1F-A4E3-47D3-B4CC-25959C439FFF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"883a18c5c28018e843d1ba9cd4acff593353170a","datavalue":{"value":"6481254","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2942880$4F3A4995-4978-455F-BA5B-EC693F9235AF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"260d20bcdb0b894f57a6beba756287ebf28a84d2","datavalue":{"value":"conversion rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q2942880$14BD4C65-129C-4970-A79D-3A3AF24862CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e22447b229c7a32c8d247e1ea4002861fd0fbd68","datavalue":{"value":"dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q2942880$1DE02CEC-6DF2-4D8B-BED5-0A84D5A8C8D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q2942880$12D98D0A-F65D-47C4-9842-51F129DB0D4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5646b3346ec7c8e6aed847c9c731c3f65ee640f9","datavalue":{"value":"tactic development","type":"string"},"datatype":"string"},"type":"statement","id":"Q2942880$9E939D62-DA6F-4A63-802B-16648915389A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2942880$6C3ECB34-9410-417A-83DA-7B6BA0E0E42F","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":"Q2942880$4D347E06-7784-4112-961F-D64F3921B372","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"896a32d5c2316f836262dcc3f79fe6fea8d9d6f1","datavalue":{"value":"https://doi.org/10.1145/2103656.2103690","type":"string"},"datatype":"url"},"type":"statement","id":"Q2942880$F1E3932D-CEEA-4674-AD9B-1DCB8D560CEE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9526f13770c9449881d779e722bcf9342226a0bd","datavalue":{"value":"W4253681328","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2942880$0C95C7B7-2F69-4AD3-8454-27F391319215","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"435c230f2e936567467c911556c7b07e730f6c8f","datavalue":{"value":{"entity-type":"item","numeric-id":2802496,"id":"Q2802496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed6aead5dd26d300f2c93c93de9b484fe8a96ad7","datavalue":{"value":{"amount":"+0.7378069162368774","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":"Q2942880$D55D49F1-A7A7-4BB6-80B1-963352E897B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2801a722fd678b19d06419d702dd97a05484198d","datavalue":{"value":{"entity-type":"item","numeric-id":5176952,"id":"Q5176952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9fb02817df7315933976db07b2b356b18dbd28d6","datavalue":{"value":{"amount":"+0.7221163511276245","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":"Q2942880$F9C91A55-23A8-40A2-A3C3-0F9AE98AD7B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c8fc519c81890f963ff41e9abebedea516f59fd","datavalue":{"value":{"entity-type":"item","numeric-id":5371944,"id":"Q5371944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3b14bcc7a5c244bfaba49c2d4f057da0474cf870","datavalue":{"value":{"amount":"+0.7196455001831055","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":"Q2942880$F7A9EC04-A744-472C-99D4-70DC0FF785F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"87d8460ce4f486383b05ac93c44ee0afdba81933","datavalue":{"value":{"entity-type":"item","numeric-id":1791152,"id":"Q1791152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae84186db83350f322917ae294951b62d5bece98","datavalue":{"value":{"amount":"+0.7162584066390991","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":"Q2942880$B2B138F2-B30B-4331-9EAC-C6F164219BCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b3e572badf5bee00e7427a40b4cef297ea325698","datavalue":{"value":{"entity-type":"item","numeric-id":5244791,"id":"Q5244791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a0e2334ec9db9bab6079b57bf82ab9540a672ddb","datavalue":{"value":{"amount":"+0.7131466865539551","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":"Q2942880$B7FE91C6-4E9D-4FB6-9401-C4010949C7C7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2942880","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2942880"}}}}}