{"entities":{"Q2879267":{"pageid":2889987,"ns":120,"title":"Item:Q2879267","lastrevid":52085384,"modified":"2026-01-20T22:02:52Z","type":"item","id":"Q2879267","labels":{"en":{"language":"en","value":"The reflective Milawa theorem prover is sound (down to the machine code that runs it)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6341496"}},"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":"Q2879267$8D87B985-2556-4F79-BC45-249CA546971F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b5a2f547802b662bcbba7bb1ff9dd4b7c8feb225","datavalue":{"value":{"text":"The Reflective Milawa Theorem Prover Is Sound","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2879267$CCA3EDC8-C42D-40F1-9568-33B2561696F3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9c352423b5d40675e0f0496a0a0d084ae89dc4f6","datavalue":{"value":"1416.68174","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879267$52453A36-D3EA-4C77-AD46-8EDA73027A9A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d5341fdbc01abc5c008c0059664648360720a576","datavalue":{"value":"10.1007/978-3-319-08970-6_27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879267$A8AFF1AB-F856-4171-B7D3-7BFFBE45BE63","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c330e55e5dc72ba4e46dcf35457734e0df28701e","datavalue":{"value":{"entity-type":"item","numeric-id":286789,"id":"Q286789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879267$D168E1FB-794F-4745-A83B-2EE94E66355E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ccf5d4548c5103107f736d99d04459a5f9188db5","datavalue":{"value":{"entity-type":"item","numeric-id":286788,"id":"Q286788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879267$5CCC2E4E-471E-4D0E-A1E4-79BD8758D1A9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879267$6D3074E6-90F9-4138-8BC0-7F9D17EE8063","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"565bc5987614f46e32dc98add32d630fe2eeb533","datavalue":{"value":{"time":"+2014-09-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2879267$5EF242CD-4B6B-4A48-830B-2655FC1ABBF6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879267$385E1268-3208-4B69-92F5-62F1C1D118D5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3b26aed9700d8b7f810ff98c362ddcc74dfea874","datavalue":{"value":"6341496","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879267$52DB86E2-8DAC-4CDB-8BF8-07E611075B35","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879267$A7F40213-6C73-4D3A-88AD-04E523CD85B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879267$591A8854-AC22-46F5-BF17-5475D87ACEB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"533959f24a509b955614f607e46b8aa4cec190ef","datavalue":{"value":{"entity-type":"item","numeric-id":20799,"id":"Q20799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879267$C73A6FE3-211B-4421-AF25-8E0CE4C9F966","rank":"normal"},{"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":"Q2879267$9DD37148-424D-4086-8063-96160674F12C","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":"Q2879267$21F0E45C-BD36-4FF9-AAC1-9C7540B9D644","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e2b0d238e0a6a1638cd6d0da521c01489812cf40","datavalue":{"value":"https://doi.org/10.1007/978-3-319-08970-6_27","type":"string"},"datatype":"url"},"type":"statement","id":"Q2879267$FE13DB55-D5D0-434F-A78D-F9D2F4361A70","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c8a85fe7d52a0446b674252c214673ef3716ebad","datavalue":{"value":"W2230207899","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879267$F7ECDBBD-4916-4C43-8864-ACC927B3311A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"da78de9f200db1e17f0d7835261a874e7380219e","datavalue":{"value":{"entity-type":"item","numeric-id":286790,"id":"Q286790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"54c46648ee0c20a499cdbf97631e443eb9de4e6a","datavalue":{"value":{"amount":"+0.9734092354774476","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":"Q2879267$DCD2DCE8-4EBD-486E-822C-8AAB6F37B5F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5c708fef69a8eece560799e6bf7db9d9dbee7964","datavalue":{"value":{"entity-type":"item","numeric-id":3088011,"id":"Q3088011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b413a609f303ede4f8c934ad81e2105ef3573d5","datavalue":{"value":{"amount":"+0.8186591863632202","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":"Q2879267$063C2CF3-4965-49DC-92A3-608EFA26BFAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8a9340227e03cb52d0a7ec16f7ac5a22cc95744b","datavalue":{"value":{"entity-type":"item","numeric-id":5327372,"id":"Q5327372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b0f42fde5b83249a3a9c6b20d937a65871e3cb25","datavalue":{"value":{"amount":"+0.7516957521438599","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":"Q2879267$C093BE5D-547F-4CC3-8A6A-6F2F12EFC5B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1cab783396284eb004b42756f108087b79277b8","datavalue":{"value":{"entity-type":"item","numeric-id":3613408,"id":"Q3613408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1a08c7f81da34d41564a00d40e9b917ad2ea00e4","datavalue":{"value":{"amount":"+0.7410297393798828","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":"Q2879267$D3324FE2-2D0A-470E-9259-0595872C9F0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"16b4ad2e93424e9b6828135c36f028dc0dcc0af4","datavalue":{"value":{"entity-type":"item","numeric-id":2219381,"id":"Q2219381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ab699035230a7866db25e4569c8b67296843dc98","datavalue":{"value":{"amount":"+0.7348122596740723","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":"Q2879267$DD9861A6-20B5-4072-8043-6E408BED3300","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2879267","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2879267"}}}}}