{"entities":{"Q832260":{"pageid":834108,"ns":120,"title":"Item:Q832260","lastrevid":64674984,"modified":"2026-04-11T21:28:29Z","type":"item","id":"Q832260","labels":{"en":{"language":"en","value":"CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7498178"}},"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":"Q832260$79ADF121-BCA0-4E5D-A72D-8D820FD52649","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"51d1c6d4183228bd5dce70259bf7326839507322","datavalue":{"value":{"text":"CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q832260$A6D061A1-1D7E-40D1-BE01-90C49B377F7D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"38d47fe4a8ccf562dbf0b473f735383ce478fb5b","datavalue":{"value":"1493.68387","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832260$F5464E53-91AC-45F3-AB60-1D935A599500","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e18ddda6086f5a4b1216ef57fbf33513d7bf42dc","datavalue":{"value":"10.1007/978-3-030-81688-9_7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832260$2E6F37DB-D152-470E-8438-39F0512CC253","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ad905386b7c3383cf03d357be2b73ba68ff5e22a","datavalue":{"value":{"entity-type":"item","numeric-id":832256,"id":"Q832256"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$DC7A9DFA-D471-427F-AA83-870BDE8A6455","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f0eb7c0b90fb0f585db1cd09c147664e442631e7","datavalue":{"value":{"entity-type":"item","numeric-id":832257,"id":"Q832257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$93364F81-2BCC-477F-B604-E075B00DEEEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"17d64add4224d48d3e6a017692fd022ede79a50f","datavalue":{"value":{"entity-type":"item","numeric-id":823307,"id":"Q823307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$16728887-99CB-4731-A0A1-E374EB5472EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3f9764996bae6bd9b17d23d85978b18dacf299f6","datavalue":{"value":{"entity-type":"item","numeric-id":832258,"id":"Q832258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$B4A9662D-3AAA-443F-9993-A20A1A6C646C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"19c17cf4b757376e81bb18052c33891da6bf831a","datavalue":{"value":{"entity-type":"item","numeric-id":832259,"id":"Q832259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$6C220F90-8105-473F-A200-D42D0D12B66D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d27ba47383ccb663a9a6898fa9f5d7c3a6d15e09","datavalue":{"value":{"entity-type":"item","numeric-id":678877,"id":"Q678877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$657B2417-DD01-4EA2-B830-FF3ED12FDFE7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"26426ab4d5a6ecfa201abc41ba9257e3996155a5","datavalue":{"value":{"time":"+2022-03-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q832260$B39EAFA2-3002-43C9-83D2-7A855EABAF57","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832260$4950F1F1-5526-416B-AC41-1F13A61EA338","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832260$ED5ABD52-279A-46DA-BBA1-601788E0FC04","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2f56879811f61838cb9fdefcd6488ab47e3b3afe","datavalue":{"value":"7498178","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832260$FB6801DC-2588-4DA4-BDF7-53D8A454D6BA","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cfc147131a7d4143ee0cffcf8574b9289d54c011","datavalue":{"value":{"entity-type":"item","numeric-id":1354213,"id":"Q1354213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$9F82F719-1E20-4617-8AB2-DB077217BFF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ddadcf23c1083cbefe0349fc4573fd061666b3e5","datavalue":{"value":{"entity-type":"item","numeric-id":1354210,"id":"Q1354210"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$1FDB5FCB-FED5-42F6-A0E3-0B3C82609272","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bd3fa568ce44545ce1c1bded3c45ecc37b43b7c1","datavalue":{"value":{"entity-type":"item","numeric-id":21467,"id":"Q21467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$A015EB60-A9B6-4DB2-8911-499ED18D809C","rank":"normal"},{"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":"Q832260$8EA349E1-4961-4672-950D-A0257DF23B1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fdab07d39556d0075d882dcfd5a58c05fcf1a7e9","datavalue":{"value":{"entity-type":"item","numeric-id":21698,"id":"Q21698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$74579736-18D4-4C61-92F4-4C182D719179","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ca3f31aa2c04d477727f6082390af9392ab5e781","datavalue":{"value":{"entity-type":"item","numeric-id":43356,"id":"Q43356"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$666DC4A7-098E-4919-8D9F-B4BC6CEE4239","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":"Q832260$CDFEEC3F-C926-424A-A55A-B1B6147201EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3ac1e8c13c0130a75f4cf78841def0133e1a8ff4","datavalue":{"value":{"entity-type":"item","numeric-id":20425,"id":"Q20425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$0A54D543-3CE0-4DD2-9562-081543712673","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e5e0ab7168ad700cf08f7688db35ed01f2d58a7d","datavalue":{"value":{"entity-type":"item","numeric-id":21834,"id":"Q21834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$F2CD71FD-FEC3-403D-B15B-4C8163F03DEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a3f7f8548c5af1e2ae512d0bcfba5384da7ef3bf","datavalue":{"value":{"entity-type":"item","numeric-id":25228,"id":"Q25228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$4756101B-D12E-4F14-89B3-E90D061258DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8bf42d0fd66acf369e3d5d44d7ebef6adc7ae452","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$BEC9C164-21CE-4C92-BBB2-44ACD7260D7B","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":"Q832260$7B7E32C2-CD66-4273-A28C-8F6AA4FF7F3B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e74791bc5ee38a5e4667311a8aeac5fd7a5e8c04","datavalue":{"value":"https://doi.org/10.1007/978-3-030-81688-9_7","type":"string"},"datatype":"url"},"type":"statement","id":"Q832260$08B4EF81-3FB8-4C34-996E-3CDAA5D51211","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5a982df3cc219b66d886c47732dab830ea64f832","datavalue":{"value":"W3183490041","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q832260$8CBF557C-D6FA-4E3A-9DEF-490D32341AF8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"efeed698c61c9d4088905eab8917123fdb73bb41","datavalue":{"value":{"entity-type":"item","numeric-id":3100212,"id":"Q3100212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$99E27CE0-0892-4248-82C5-1302ADA1C3B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60159374e2e3f1fa60e69dc94c949ae9174a77c0","datavalue":{"value":{"entity-type":"item","numeric-id":5308405,"id":"Q5308405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$293F0CFC-DCB7-4FA3-8324-C4CEFB286A9C","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":"Q832260$D3EE8EF2-1D7C-4908-B806-014A7D680112","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cba1d07dae14cc5134ffc3788a13ade150ee8b4a","datavalue":{"value":{"entity-type":"item","numeric-id":3460065,"id":"Q3460065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$137F84DC-2180-46D4-9466-0C919DA34009","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e4aed9b8c360dba198361b37afc63de7b6c5158","datavalue":{"value":{"entity-type":"item","numeric-id":5920089,"id":"Q5920089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$8B5B9A80-476F-4623-8B1A-8928DD91B939","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c18f6d1d44ef740fcb363b3e7b055f66c3e3376b","datavalue":{"value":{"entity-type":"item","numeric-id":1791180,"id":"Q1791180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$265D1A27-A232-4B88-97E9-2FBB82B6C232","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$786413D4-5301-4B75-82DF-DF4D131E5263","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2df574c1c197598a7866c590ecc33f5913307b7","datavalue":{"value":{"entity-type":"item","numeric-id":2181940,"id":"Q2181940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$695A691F-BF8B-4357-AA71-B3F45C8E1EE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8963c27a223020a3d0ab46c3570fab93816de414","datavalue":{"value":{"entity-type":"item","numeric-id":5009416,"id":"Q5009416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$E72713F8-3447-4E3B-9F73-E56F4E49C3B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dee09e75a430fc0be911c9a36f98899b21bf0296","datavalue":{"value":{"entity-type":"item","numeric-id":2441776,"id":"Q2441776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$A3098E65-A5CB-4E32-9652-3694383002CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb081c24d3f308759ffc5be25d93bb06a52b464f","datavalue":{"value":{"entity-type":"item","numeric-id":3192088,"id":"Q3192088"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$2D97A2B1-0214-4AC8-9D7A-AE6ED3244CFE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8738b00b1ca33051359a5e295052e5443121b0d9","datavalue":{"value":{"entity-type":"item","numeric-id":2164216,"id":"Q2164216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"211a7939baaf405098e31ff6214e049f9e5cf46b","datavalue":{"value":{"amount":"+0.7774263024330139","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":"Q832260$0F1F8A9F-75E3-4B79-8F74-EF1940A022C1","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":"3afb6b33864c1920c43e864290f1e79173b6fc57","datavalue":{"value":{"amount":"+0.7676469087600708","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":"Q832260$E61669A1-1BB2-4B39-9CBD-05300B78619F","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":"93c7062392889e74f72be63c6846beca1732372a","datavalue":{"value":{"amount":"+0.7453853487968445","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":"Q832260$015480E4-91DB-45E5-824A-27D19C2F2244","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"297d7ca756a0fe9edb01e6c2d45d7d8ced12f185","datavalue":{"value":{"entity-type":"item","numeric-id":3088005,"id":"Q3088005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"38c808a5229e44b0e2cacdbaadebcb744183bbef","datavalue":{"value":{"amount":"+0.7237398028373718","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":"Q832260$EC8E3860-EAE1-4B84-A5C5-1A2485AE5322","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fa0c8580ce4e0cb685d0ff86138835bcfa17cf41","datavalue":{"value":{"entity-type":"item","numeric-id":3100209,"id":"Q3100209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8381946fc50a08c1e546488fe964c45331eb54ff","datavalue":{"value":{"amount":"+0.71949303150177","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":"Q832260$481B700B-0C0D-4AA3-907A-E45B7485E238","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q832260$62C251C1-5422-4554-8E5C-5271B0587C7F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/CoqQFBV:_a_scalable_certified_SMT_quantifier-free_bit-vector_solver"}}}}}