{"entities":{"Q3100212":{"pageid":3110927,"ns":120,"title":"Item:Q3100212","lastrevid":86477342,"modified":"2026-06-03T22:17:49Z","type":"item","id":"Q3100212","labels":{"en":{"language":"en","value":"Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5977512"}},"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":"Q3100212$F2E33B27-CF55-4F80-9E5F-0059DE6ECCD1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"82d7c531165abb82dcfa84e09cff6edee0293d1d","datavalue":{"value":{"text":"Reconstruction of Z3\u2019s Bit-Vector Proofs in HOL4 and Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3100212$BA829684-9FE6-475C-BC24-8B6BA1194464","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"56de5be8191c2c026dd4b4521b2fae9591d916d7","datavalue":{"value":"1350.68225","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100212$08CA4A08-AE45-4C08-8984-00C33FD63D6C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"502cbd33b25e09b87652e74c7f9f3c646cb7ab82","datavalue":{"value":"10.1007/978-3-642-25379-9_15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100212$0FCFFF4A-1DA0-427D-A249-F79F3323262B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e52ea9fecc32655489a0560f1f3a2c96d34140f0","datavalue":{"value":{"entity-type":"item","numeric-id":287336,"id":"Q287336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$936289A4-9D60-43C6-921E-3B4EC1E97D05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"30e84c1c161a78deee54f35997c4f862ecf81aa5","datavalue":{"value":{"entity-type":"item","numeric-id":172359,"id":"Q172359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$292E9019-5C14-4C75-9C91-8795B0773E76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"50d312af30877232f30bb9c23fdc31fcdcb768e4","datavalue":{"value":{"entity-type":"item","numeric-id":2631536,"id":"Q2631536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$7ED53671-2A5A-4191-AFEB-86095AD19787","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d1f8cd3b806fd78547b3f4844ba487e41a5ec455","datavalue":{"value":{"entity-type":"item","numeric-id":286783,"id":"Q286783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$C22DA549-732B-4D43-B0E4-B9675B5CE661","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"19e7468504fbcb9c3a09d3a38cdd67d03e02eec6","datavalue":{"value":{"entity-type":"item","numeric-id":2938035,"id":"Q2938035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$4D1A36E1-E415-41BD-BACD-DA57B5530513","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6d06d6de084d6566994eb3940381939ab0e2877d","datavalue":{"value":{"time":"+2011-11-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3100212$EC647EE3-8339-4441-933E-DD565858823D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100212$D4CA9A56-CBC5-4464-8BB4-26D340C66CFC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ce76628fe75b043f36177160be293196f41d1388","datavalue":{"value":"5977512","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100212$D697F73D-4614-48B6-953C-5695DEA6F0E2","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"75051848b474128e4985ed4bd6de9dfa91223569","datavalue":{"value":{"entity-type":"item","numeric-id":18412,"id":"Q18412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$D46EA898-D179-44B6-9722-990952085046","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":"Q3100212$F0F04EFB-ADAA-45B0-8172-0E3D36E157C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$048DF45B-0B5C-4770-8D79-C34A89B344F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4c394b74049cbdb0cef88807aac9fa3513bba728","datavalue":{"value":{"entity-type":"item","numeric-id":13169,"id":"Q13169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$79B244DE-2A0C-4C3B-BA94-76450D76A9C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$AF035376-82EF-4A53-9C81-34E5884DAD84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$9BDA9C24-9F69-4134-A7C5-A320C5019B19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9b0860d94af5fdff4b5635709ae334aacdf07ca1","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$681EEC05-513F-4218-828E-2D537A815980","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cd543fd49199b1838ba332ea5e7b335fbe6c5a58","datavalue":{"value":{"entity-type":"item","numeric-id":19608,"id":"Q19608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$E6A9D9E1-AC13-4D69-A3A3-80A0DDCE3C5C","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":"Q3100212$61F58EDC-904A-47E9-88D4-243598335D5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$80A1A029-8796-4E10-8B4F-DAAB4C606F71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6d1b503d7c8f19634e207574177819c306621855","datavalue":{"value":{"entity-type":"item","numeric-id":17038,"id":"Q17038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$04ABBF62-969B-4C26-BF99-C967B7719A25","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":"Q3100212$CB65C6DE-28BC-433A-A838-980F4E2DD040","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"edab751d71527c4da89157d59dcba9d9fd4c2898","datavalue":{"value":"https://doi.org/10.1007/978-3-642-25379-9_15","type":"string"},"datatype":"url"},"type":"statement","id":"Q3100212$2843A46B-DD51-40EC-A8DF-86400C9F72BB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"edd0eec86bd9871e2f5cdb808f2e3fc95bafa63b","datavalue":{"value":"W197756383","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3100212$7784F977-2A48-4C53-8344-0A1A7EA8D9DD","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"999b66e467dc75475554ffc802596b0ddbf62a9e","datavalue":{"value":{"entity-type":"item","numeric-id":1040776,"id":"Q1040776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$0DBF142C-EB46-4EC6-AACD-FB73B2BAA78D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd9ea7887150abfd8958ac46eef7ddf839a8f58f","datavalue":{"value":{"entity-type":"item","numeric-id":3543643,"id":"Q3543643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$C3BAE769-2DC4-4C26-BCEB-91CEBE7672C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3fea6dff3d36407dad60fa8e8c9bcc1f06ec22da","datavalue":{"value":{"entity-type":"item","numeric-id":5200019,"id":"Q5200019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$96A20EFE-3A94-4E00-871C-47BF5118362F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8814f08a007eccd0762345bdf06bc2170a9f2f1b","datavalue":{"value":{"entity-type":"item","numeric-id":2655335,"id":"Q2655335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$CD7AACE2-B835-4DBA-89A8-00658C63D919","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"494aa31720bff090f87eabeb86ce7380ba058cbf","datavalue":{"value":{"entity-type":"item","numeric-id":5747649,"id":"Q5747649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$595C3EBE-F137-4DDA-B8A5-7BE3084818E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2b783d0052b7f250a9573410e9be2b4624ef11e","datavalue":{"value":{"entity-type":"item","numeric-id":5899057,"id":"Q5899057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$92B33D33-CFA7-41B6-A82D-CA2B78281A69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b43a25ba24825d35a343ae255abd617023e5daad","datavalue":{"value":{"entity-type":"item","numeric-id":5200028,"id":"Q5200028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$BD3995D1-78D5-4719-95C1-B48EEAD2D674","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"879dcd858f7bcfe1ef3910bf97ce3d345da5b737","datavalue":{"value":{"entity-type":"item","numeric-id":3088019,"id":"Q3088019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$1BDB9161-1891-4187-A3C8-C12CDB3DD77C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc8abb92210655a5bd4143cbbadd6eadb52d635","datavalue":{"value":{"entity-type":"item","numeric-id":1801222,"id":"Q1801222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$77CFD9EF-0656-4424-8AD9-28DFD89EEF00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14533123e0b9e73c06f9737a070ee002c25f5f1b","datavalue":{"value":{"entity-type":"item","numeric-id":3612442,"id":"Q3612442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$BEF58EB5-5BC7-4E8D-B649-CAB835D0D767","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a5e182d22cd63374751049cb1ad374f0b5175f7","datavalue":{"value":{"entity-type":"item","numeric-id":5477650,"id":"Q5477650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$4D9A4F74-292E-4D61-BD55-2160756099C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"76f085e060cc02117b4ec73931c77617da801d17","datavalue":{"value":{"entity-type":"item","numeric-id":2473386,"id":"Q2473386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$4252C88F-12FF-49D6-8D44-439A2563AE3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6b26606a781175a19b1c8fcba43abdeea964791","datavalue":{"value":{"entity-type":"item","numeric-id":2848688,"id":"Q2848688"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$080E748E-7E5E-417F-B9F4-A7A64070D6B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"271326b3f6ba4699b8b9534f6c64338c8ddd3a50","datavalue":{"value":{"entity-type":"item","numeric-id":1006729,"id":"Q1006729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$26B15677-70E2-4EE3-A05F-B5C54A86D39C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e1cf1fbb097a93619e873e24271fa9638a00cf8d","datavalue":{"value":{"entity-type":"item","numeric-id":2441770,"id":"Q2441770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$92AEBAE3-0BFE-41DD-B120-94AAC52B7D1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2667127ff7e04fad7bf3f88432b6dcb7791cab15","datavalue":{"value":{"entity-type":"item","numeric-id":3624141,"id":"Q3624141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3100212$942AFFD4-C747-4A9A-922A-E44624E4D535","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0b4f75f494f6421c325356fd1ed820027bfc297a","datavalue":{"value":{"entity-type":"item","numeric-id":5747649,"id":"Q5747649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10f3656708f4e27c07838f80a9077445e5da3cdf","datavalue":{"value":{"amount":"+0.8807467222213745","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":"Q3100212$00B6C66E-DB85-4DAE-885F-80C036D304C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d13a1aa7335cec291b0dfd74d25004b6bcf26c1d","datavalue":{"value":{"entity-type":"item","numeric-id":3460065,"id":"Q3460065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a16deae84afa360bcd6e86f8ac91a68f9043a80b","datavalue":{"value":{"amount":"+0.8047136664390564","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":"Q3100212$C566E0B2-93EC-48D7-ACA3-01AD32393BFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"07f00829899bb29edaf603e18e1a2afbc1c56b2a","datavalue":{"value":{"entity-type":"item","numeric-id":3088019,"id":"Q3088019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3ac46cad0ecbf3cfff64d0186069bcc32e90107c","datavalue":{"value":{"amount":"+0.79438316822052","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":"Q3100212$F8FE91DD-51D1-421F-BD86-7F7291170ECB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1911663a64677dd41e915eba33d6d9370e47ba6a","datavalue":{"value":{"entity-type":"item","numeric-id":2181940,"id":"Q2181940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e3c62fd3cc2cd9fa235940e3506154c279e69fc6","datavalue":{"value":{"amount":"+0.775866687297821","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":"Q3100212$A4FEFAE8-D4B0-4CA2-85E4-6B27208457F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2be33ccab093ca2a6b6fd2b7057b69ca7524c000","datavalue":{"value":{"entity-type":"item","numeric-id":606999,"id":"Q606999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"09b63510ce4c3f563e875f9bbb82ec1656c0a8f8","datavalue":{"value":{"amount":"+0.7678532004356384","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":"Q3100212$64727937-7D89-4BB9-9E7B-B864DE65946B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Reconstruction_of_Z3%27s_bit-vector_proofs_in_HOL4_and_Isabelle/HOL"}}}}}