{"entities":{"Q5758122":{"pageid":7787673,"ns":120,"title":"Item:Q5758122","lastrevid":97356821,"modified":"2026-06-05T14:32:03Z","type":"item","id":"Q5758122","labels":{"en":{"language":"en","value":"Deciding Bit-Vector Arithmetic with Abstraction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5185791"}},"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":"Q5758122$FBE24584-54C0-4351-B5B9-59BED7DF65E0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"477173638e399f5491e7b75bddf5cfc2969ee512","datavalue":{"value":{"text":"Deciding Bit-Vector Arithmetic with Abstraction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5758122$76755EE0-63CC-42BB-8D1E-84D2E2FB7992","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bbf5d382e6ff58b6332bd50c9ccb825c4a9fce6a","datavalue":{"value":"1186.68281","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5758122$C62D6C8E-4744-47CC-A6D9-F77F19778693","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f60a1dabbd1e41730980e23798ba20a6bf3babf6","datavalue":{"value":"10.1007/978-3-540-71209-1_28","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5758122$9E344038-4C72-47B1-865D-EB0DE3503D4E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a2c27d3e0e0b5520ffb8ac40111c3ffad759a39f","datavalue":{"value":{"entity-type":"item","numeric-id":1426129,"id":"Q1426129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758122$804E8607-0129-47E0-95D5-FBDC983DFBDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"de4a775b741b129661b3807102896dab39bea660","datavalue":{"value":{"entity-type":"item","numeric-id":438554,"id":"Q438554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758122$2CC07F34-A9A4-486C-A320-A342237222EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8dacfcf053d2b6145a7d8f294969b0cd4cf897e3","datavalue":{"value":{"entity-type":"item","numeric-id":436422,"id":"Q436422"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758122$696DF6AE-C244-40CF-80C7-8A3DD718D10E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"55f249f40c4f258debe6dc3dacc160f2e23026fd","datavalue":{"value":{"entity-type":"item","numeric-id":557794,"id":"Q557794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758122$406A9B57-05DD-46DA-87C4-18E6ED806CB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"521ea2cb6a301fe9f22d88a2561e7746fdb48379","datavalue":{"value":{"entity-type":"item","numeric-id":246145,"id":"Q246145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758122$93244B49-95E0-4C67-997A-EFB07B72DD4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"25a96a4a82f8fdc1c02239fa7e8a578b0c486015","datavalue":{"value":{"entity-type":"item","numeric-id":3510847,"id":"Q3510847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758122$3E57B805-4D28-44D9-9CE8-4A4B25C15237","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0caef843b05c7cfb5667c1a8106613cbf61a6d23","datavalue":{"value":{"entity-type":"item","numeric-id":2894263,"id":"Q2894263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758122$DE137704-CEBF-48C0-8B8F-E7752046427D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d4ccb5809271d2f0bf96f65b85084aa847fe92ef","datavalue":{"value":{"time":"+2007-09-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5758122$0894C833-A776-4085-9113-A01B97746DB8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5758122$60779853-787B-4DE5-97CD-2D716D278873","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0bf6965fe5c75a74136cb1391e53edce5a7de2b0","datavalue":{"value":"5185791","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5758122$98107CA2-922B-44D5-9046-9B52B4378DEB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7a35a47cef9f2baec76c3bfc2bf8f6032431cb1c","datavalue":{"value":{"entity-type":"item","numeric-id":16827,"id":"Q16827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758122$87B3B81F-4F83-478D-A123-8F27AD37109C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d650a7af9fdbfa854d490255d18c32cbaf84928c","datavalue":{"value":{"entity-type":"item","numeric-id":16925,"id":"Q16925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758122$51DACE15-2ACB-4D73-A602-BDF21F7AF7FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"86b4d5730b37b9917aebaffbab7ba473acfa7fcf","datavalue":{"value":{"entity-type":"item","numeric-id":14040,"id":"Q14040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758122$49858E91-1DC5-4902-B333-7D8699B2F935","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8449db7d9aaa28101ba7b0de8e98d9c446365070","datavalue":{"value":{"entity-type":"item","numeric-id":13332,"id":"Q13332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758122$48829A64-15C6-4B88-8B70-F899BD8B179D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"85575b60ef4d0a8413d3c895be2530b8915bc3fb","datavalue":{"value":{"entity-type":"item","numeric-id":16612,"id":"Q16612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758122$EBAD0508-34AA-4860-B879-3015F905CDDD","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":"Q5758122$52E2BF1F-AD3B-413E-B64E-FCA24D1F48BC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"459bc5dafd7fb5045df510ed9ba97f63d949dd26","datavalue":{"value":"https://doi.org/10.1007/978-3-540-71209-1_28","type":"string"},"datatype":"url"},"type":"statement","id":"Q5758122$9B28C1C4-9F10-4E5A-B5C1-AA0EF176C1A7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7f49db31694855e774f5688139cc354bbaa06fb2","datavalue":{"value":"W1919297764","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5758122$487CA790-6FAF-43A0-A243-1AC25CD65292","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5f17fbff8582b39405885d1adaa6e24599c57537","datavalue":{"value":{"entity-type":"item","numeric-id":5429343,"id":"Q5429343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"17b847189713c68dd73695182292593c30ce4753","datavalue":{"value":{"amount":"+0.8218294978141785","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":"Q5758122$DB6874FE-84F8-4CFC-B829-52965416E62B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e800ae413452d6d975b451d64218c5d97edbb067","datavalue":{"value":{"entity-type":"item","numeric-id":1623140,"id":"Q1623140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e600cdedb1fb7343910b8c2fef02434b5a14617b","datavalue":{"value":{"amount":"+0.795462965965271","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":"Q5758122$DC7968F9-63AF-4766-BE6F-23A2F95FCAD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b411317991d275735a47e6906cb73deffb4a3f47","datavalue":{"value":{"entity-type":"item","numeric-id":2818018,"id":"Q2818018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"30021bf1d6afdac36588c7671e59b4b714ff1d60","datavalue":{"value":{"amount":"+0.7903607487678528","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":"Q5758122$CDA57D49-4272-4EF2-BF5B-2A88D675794F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"62083930072469fced44076a39fcd523a4bfbfbd","datavalue":{"value":{"entity-type":"item","numeric-id":2152654,"id":"Q2152654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53b0801bf1890783e1a43163ea25d5e10208e5b7","datavalue":{"value":{"amount":"+0.7808107137680054","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":"Q5758122$CB362A10-D41C-4488-8945-961F31CCEC37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ba2dd67d9904f8497b4b7b4ba2781e1ac9bb002f","datavalue":{"value":{"entity-type":"item","numeric-id":2818019,"id":"Q2818019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c7bcba60c81a18046b9772b96cb39b5537ebb853","datavalue":{"value":{"amount":"+0.7793748378753662","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":"Q5758122$2A73998A-1F2D-47A7-BB9B-4A6F1389C7B5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Deciding Bit-Vector Arithmetic with Abstraction","badges":[]}}}}}