{"entities":{"Q6041273":{"pageid":13175374,"ns":120,"title":"Item:Q6041273","lastrevid":47854108,"modified":"2026-01-02T21:33:57Z","type":"item","id":"Q6041273","labels":{"en":{"language":"en","value":"Validating safety arguments with Lean"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7689379"}},"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":"Q6041273$1D1CDE37-8250-4B82-88FE-ECE5BC2BC3F7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2b33f7d7ee435d60eb2e722e68cbe52709c0d2ae","datavalue":{"value":{"text":"Validating safety arguments with Lean","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6041273$70C2B0C0-2A40-4A91-8C63-CAE93833E566","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ac4ea2a64e58d0f923826020b0676bf36810b274","datavalue":{"value":"1522.68337","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6041273$37167246-C817-4EB6-8B3F-FDDDBADC77E9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"087b08c6a77508f1788682175251fa5bb97ae6bc","datavalue":{"value":"10.1007/978-3-030-92124-8_2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6041273$16D07B05-2C64-4B46-BF28-5982A7017862","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7f21f66ce8715c2c9dec956e78c8b66a8b420e23","datavalue":{"value":{"entity-type":"item","numeric-id":6041269,"id":"Q6041269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6041273$72129695-E2F9-4418-BFB0-8E0CD346334D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6ed9f27d1ed070e20a09d213c5065369df28261f","datavalue":{"value":{"entity-type":"item","numeric-id":6041270,"id":"Q6041270"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6041273$884FB733-47E6-4DE3-AC58-CC42D84EB973","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dec383fe64cad6b8480a51d7fed15ba38d66988f","datavalue":{"value":{"entity-type":"item","numeric-id":6041271,"id":"Q6041271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6041273$6D2743B4-1334-4CA6-8C54-6D2C983B8C74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c4e3ff4936658f2ac70d17de73ad3827f7ec3cee","datavalue":{"value":{"entity-type":"item","numeric-id":6041272,"id":"Q6041272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6041273$64C6F645-C438-4310-8662-C2D46FA61608","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"794c304803c228a1c8e63e5a19cfb840dd5c432c","datavalue":{"value":{"entity-type":"item","numeric-id":488217,"id":"Q488217"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6041273$3D99964F-249B-4CDC-B123-5EC14ED9CEB1","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a8f5cbf6360429635db718a7502a7494a9026ef3","datavalue":{"value":{"entity-type":"item","numeric-id":3095231,"id":"Q3095231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6041273$F5D4377E-5DF8-4C96-AF37-0EF0224B9CDE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9e202514302232ff7f5ec81097f072c587f02b43","datavalue":{"value":{"time":"+2023-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6041273$95B1150D-B862-4158-A3BE-CF6AB6B80BBD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6041273$AB32F60F-2D20-40B8-8E31-8E624D18A5D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6041273$0C9426C6-1A2A-4F1A-BA98-9DE831AB5255","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6041273$53319150-164E-4781-97D8-DF48D55F9D3A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7cd259deb1d6ac1434f9f4783cd9b69d33e45097","datavalue":{"value":"7689379","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6041273$D3359CB0-5B86-4F00-A318-9B03C159CFBA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6b4da7330bcfdc40e38f4c00fc70aebe2981f38c","datavalue":{"value":"assurance","type":"string"},"datatype":"string"},"type":"statement","id":"Q6041273$72E0C434-B08D-42E9-BCDD-59C8CC08AC5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"624e71aa223bb56c4bdcfd4d4c154f9d5a6f325e","datavalue":{"value":"safety cases","type":"string"},"datatype":"string"},"type":"statement","id":"Q6041273$EFDB6F63-050B-4ACF-AF96-F3EB677A6A25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"98b5b5a4f0c825ea91b5dc8ad46045a364b8968b","datavalue":{"value":"strategies","type":"string"},"datatype":"string"},"type":"statement","id":"Q6041273$6F4DADDB-D6BF-4005-B6C8-BDF0D8A842B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6041273$E2FBAA17-5FF8-4EFC-B184-077C27F721DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4e8fd89fa28c0f6c3672ef10c3a2104586281edb","datavalue":{"value":"Lean","type":"string"},"datatype":"string"},"type":"statement","id":"Q6041273$47013B51-63B6-4E50-AC4A-B30BFF5657D6","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":"Q6041273$77697267-2FC8-4AAB-A29E-2070B8F9D89A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"efe264d271ce9107ef52f2dc76c2fd6b76229eb3","datavalue":{"value":"https://doi.org/10.1007/978-3-030-92124-8_2","type":"string"},"datatype":"url"},"type":"statement","id":"Q6041273$D7FB8791-0D71-47E2-913A-0B7406B88EDD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3d2f499180158b8c1bcf7bc630c96cfae94d5c22","datavalue":{"value":"W4206207168","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6041273$49F61DE7-9A93-4147-9D0F-4F7316992BF2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d84ade6a02bd73f79c254069b90a11e1d3dc467","datavalue":{"value":{"entity-type":"item","numeric-id":4095835,"id":"Q4095835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6041273$7BA94C19-4A34-4028-BA90-7B662CE2A8EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"333782dfe2a782886768e8c7561d4e8bfd035e1a","datavalue":{"value":{"entity-type":"item","numeric-id":2655327,"id":"Q2655327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6041273$5A2E2E10-9E26-4348-902E-EF9127AA8E17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8242928870aab67343ad0152eb7ca8357168f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6041273$3B9BE1BF-6208-4EB4-B339-DBC143A262A5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"33d57548efb48beca15cf0e2f6e4841ea85652b2","datavalue":{"value":{"entity-type":"item","numeric-id":6486019,"id":"Q6486019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c231dcb99cadcba2d2441eebe8b142694b45dd7","datavalue":{"value":{"amount":"+0.7271740436553955","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":"Q6041273$95077CBE-603E-4CC4-9FE3-611868A07849","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b990aa57577ff891a3d2a0c215b69df488c1800","datavalue":{"value":{"entity-type":"item","numeric-id":2065527,"id":"Q2065527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"749e74e90d60293494e992ddd2e0df9a94300b3e","datavalue":{"value":{"amount":"+0.7188423871994019","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":"Q6041273$175D1606-CCB2-4CA7-9BAB-D7F9F1AB82A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"79f717f1a22a64fa936392f7c6dee8bfd093ec25","datavalue":{"value":{"entity-type":"item","numeric-id":1649603,"id":"Q1649603"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"364766dfeb957e2f4224f2c180574d402cc2284a","datavalue":{"value":{"amount":"+0.6508669257164001","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":"Q6041273$22B1F133-15AA-47D5-AEAB-875F3128E835","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"41b4ad3d077d16d9141a48af1855cc2686cdbeda","datavalue":{"value":{"entity-type":"item","numeric-id":2329596,"id":"Q2329596"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"77883a4b67e001b66683bfb2bb10e7ec1f43ba90","datavalue":{"value":{"amount":"+0.6480534076690674","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":"Q6041273$49F048DD-4A1F-484F-87E9-985CDA126A95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"99eab32cc992f7b06131ec37f0a1c6cc8e0fb2ff","datavalue":{"value":{"entity-type":"item","numeric-id":4738429,"id":"Q4738429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"30d3de4c45d37a67e057628070d701234a83a688","datavalue":{"value":{"amount":"+0.6388523578643799","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":"Q6041273$DB9F0D7B-24EB-4807-859B-6A2FEAFC2F75","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6041273","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6041273"}}}}}