{"entities":{"Q3095242":{"pageid":3105957,"ns":120,"title":"Item:Q3095242","lastrevid":51357302,"modified":"2026-01-17T22:05:50Z","type":"item","id":"Q3095242","labels":{"en":{"language":"en","value":"Verifying B proof rules using deep embedding and automated theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5965363"}},"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":"Q3095242$5964C4B4-58C3-4A8D-A916-7DE086C48528","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4ff38a167f90a54cd7b69d2df14630dab856480e","datavalue":{"value":{"text":"Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3095242$445897E2-2369-4FA5-9E83-783ED29AB1C4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d6e62c32922c3100c8e6779fe75f3dc1e27d31e3","datavalue":{"value":"1350.68236","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3095242$156C7565-BA91-42D3-9027-B3C8E4CB8E31","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"988dd96be243e74b962f7aed591d940ca57d4801","datavalue":{"value":"10.1007/978-3-642-24690-6_18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3095242$4973E06C-89C6-4D04-A6EC-8EC3EA812D99","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e6f0f3a64aeacf8071e0f9dbdba25c8a0eb127ea","datavalue":{"value":{"entity-type":"item","numeric-id":2908503,"id":"Q2908503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3095242$EE8C6002-40C1-4DF8-A779-BFA28F9124C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5c4c2fcb6c198441ad0b64612ab548e3aaf3782c","datavalue":{"value":{"entity-type":"item","numeric-id":2908504,"id":"Q2908504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3095242$59B456B4-F2F7-425F-AE4D-8122C3C44131","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"786f6c8f2a36da61e98b228bbd36b74e25ad6f92","datavalue":{"value":{"entity-type":"item","numeric-id":2104524,"id":"Q2104524"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3095242$7DFA3A38-4D73-4950-AA15-1D9245C99EEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f8c40e2cd3207dd1d19085f0b79e8fee7be86ced","datavalue":{"value":{"entity-type":"item","numeric-id":1624591,"id":"Q1624591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3095242$3C8A74BC-6AAD-4465-8305-9657814833F0","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":"Q3095242$7456AFA4-4E47-49E0-886F-C7A2E014E3CD","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2900c2786b097edbfba1608d72278b11f29ad22b","datavalue":{"value":{"time":"+2011-10-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3095242$B8783E65-92ED-40C7-B112-54937DBBB3CC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3095242$3BA90E21-5B74-405A-A8D9-AA369D989916","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3095242$6C73699F-0357-4A28-A958-81F7ACE531C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3095242$88748B20-13B6-4F7B-94E2-4271C88B595C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7b1fcf32b17c80563d67c8c24053f40422f92aa3","datavalue":{"value":"5965363","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3095242$3ACC127F-0305-4C37-803B-383ED5EE841E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ab5c99825fc3750d24a6d5e8f9dc34ef12c1bf4f","datavalue":{"value":"B method","type":"string"},"datatype":"string"},"type":"statement","id":"Q3095242$E8AD9EA5-6D64-457B-9E08-F0F129B0A9C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3719ed41893672db063f7cdecb5bcd68172db4a4","datavalue":{"value":"proof rules","type":"string"},"datatype":"string"},"type":"statement","id":"Q3095242$963807CF-A815-4CC8-98BD-AAEEE934F981","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q3095242$596C797D-D54A-44A5-BCCE-AE5842D96BD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c1eb112edcb1c678c9102344762b64b2d9359622","datavalue":{"value":"deep embedding","type":"string"},"datatype":"string"},"type":"statement","id":"Q3095242$BA4A4F32-578C-4966-9316-35E340D5A10C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3095242$C2B931DD-5F04-4D7A-8585-D786160D2708","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q3095242$104072AA-1A73-45D3-8136-7EBCB0BA34C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"28123a0147c4696e26504aa90d2d325065e4032d","datavalue":{"value":"Zenon","type":"string"},"datatype":"string"},"type":"statement","id":"Q3095242$D4DD3939-2BCE-4FA3-901A-0756E1016670","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":"Q3095242$7F2F87D4-46AA-4C54-BFC0-5CC1B1B5F6F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e3fa1be4925f6565903e34254fe3ce3cb99beabc","datavalue":{"value":{"entity-type":"item","numeric-id":18828,"id":"Q18828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3095242$C40C34FB-6F2F-4775-9624-B9821BE06D07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3095242$6E56967A-5879-4FC8-B444-E43E71DB35FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"acd0a7f965bd7a2eea8391d50182b3fc185bc6de","datavalue":{"value":{"entity-type":"item","numeric-id":19144,"id":"Q19144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3095242$6394A550-C7DB-41DD-B3D7-1EC37074747D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1017108dce3983431546a14c274f65bc4aaae70b","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3095242$820399B4-0CE6-4F2C-86E1-7D83B3D2B23F","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":"Q3095242$21B09061-CA7C-470D-9294-3D760489E4AF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"478360200295c8e871e99c6fb71fcc5f0159ab32","datavalue":{"value":"https://doi.org/10.1007/978-3-642-24690-6_18","type":"string"},"datatype":"url"},"type":"statement","id":"Q3095242$3DEF089D-75A2-48F9-BC0A-C5CE1CF97287","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3f5c237a42a0e46bc2d57e5952411ae769052cfe","datavalue":{"value":"W2213028572","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3095242$9770AFAA-94C1-4347-8BA9-BEE2FBDB2CE4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae170f67b5a99f655b51707d2e6917e4913c4d7a","datavalue":{"value":{"entity-type":"item","numeric-id":4208552,"id":"Q4208552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3095242$8438F67F-56E6-4F95-ADB9-9C0D0B60259E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a8db0c9d2e475257c3fad4546177506b22344b3","datavalue":{"value":{"entity-type":"item","numeric-id":4472186,"id":"Q4472186"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3095242$26540436-46E6-4251-89AB-E4F34BEF7A39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4370175d8030918ba7fe1c9ab8112224b76824d","datavalue":{"value":{"entity-type":"item","numeric-id":3498463,"id":"Q3498463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3095242$88A104A2-E932-463B-8E2C-B325C2CBB01F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"526569e2045d88153ecb5cf7f75a680cdcd5a85b","datavalue":{"value":{"entity-type":"item","numeric-id":2767010,"id":"Q2767010"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3095242$4311CED8-6321-49AB-B063-A5E21452529D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58ca6fa462c5ab7c65a93ca673783dd3368bdc6a","datavalue":{"value":{"entity-type":"item","numeric-id":3498474,"id":"Q3498474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3095242$79329090-C659-4811-89D9-47BA30AD25C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a8a35c717a135c35af34cf713d071a53f3bce578","datavalue":{"value":{"entity-type":"item","numeric-id":4472180,"id":"Q4472180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3095242$D5EF457B-6E43-4CF1-B8BC-8E0FBD2C893B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0809d9b1dd704b43e96f40cadc787982dd501a12","datavalue":{"value":{"entity-type":"item","numeric-id":2908505,"id":"Q2908505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59e07dbcf1da6911ba1472d22614a1bfdc0f3412","datavalue":{"value":{"amount":"+0.7607758045196533","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":"Q3095242$E87A481C-4B46-409B-991E-E96BD7449AC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e1457e45d20c22c5f195afe93266c0957a2f0e8d","datavalue":{"value":{"entity-type":"item","numeric-id":3179401,"id":"Q3179401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb9e6502bedd818d06eae4a29dfcc054c0fc7dca","datavalue":{"value":{"amount":"+0.7425916790962219","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":"Q3095242$9B722E8A-F93E-4DD5-92A9-9533DDC73BF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9585d6dc413cb5570dd2aa511774e197ff89992b","datavalue":{"value":{"entity-type":"item","numeric-id":3498474,"id":"Q3498474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"525d7b8cc30ad0817c156d30bb0b16cfe7486e8a","datavalue":{"value":{"amount":"+0.7285917401313782","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":"Q3095242$EB5D9BB2-5F4C-44C5-8FFA-53634DBF108F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5e0cd586aabf9acc9c187a4478f99035269342aa","datavalue":{"value":{"entity-type":"item","numeric-id":5179355,"id":"Q5179355"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ee4e1442bbb8af4ee0b8d285552d8d63a52cc1b8","datavalue":{"value":{"amount":"+0.7035393714904785","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":"Q3095242$EB4BD492-6FCA-451A-B921-80596BF56E83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"27834f8881d79d504650b55693f4830b894523f6","datavalue":{"value":{"entity-type":"item","numeric-id":4530805,"id":"Q4530805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"09538d2906f6b7e6a0424fadd278ca1417cb59b1","datavalue":{"value":{"amount":"+0.7021380662918091","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":"Q3095242$1FBC608B-C78B-4CD7-8DB3-5D2B2F222CD1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3095242","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3095242"}}}}}