{"entities":{"Q6165889":{"pageid":13300771,"ns":120,"title":"Item:Q6165889","lastrevid":102442970,"modified":"2026-06-06T04:28:24Z","type":"item","id":"Q6165889","labels":{"en":{"language":"en","value":"Constraint reusing and \\(k\\)-induction for three-valued bounded model checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7721150"}},"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":"Q6165889$5CE80678-13B4-4E81-BFDF-092B3FDA62C8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4abfd0c29716a8cfdf0d23f04933ac5f03dcc7fe","datavalue":{"value":{"text":"Constraint reusing and \\(k\\)-induction for three-valued bounded model checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6165889$94288ABB-4F56-4375-B2ED-3934531878BD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"012d617fa552d4b2817b7d7f62e5d3edbbe2a0cc","datavalue":{"value":"1519.68142","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6165889$D8B54701-4817-41FB-9699-C1F235A75C98","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"99b5225733b538e8d2429a5704f8209353f83901","datavalue":{"value":"10.1007/978-3-030-03044-5_9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6165889$B2D2544A-AA39-43E6-B0FC-ED767C7A82C1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"24ded8c8d541f1e4a4b945a9397a18dce6ec659e","datavalue":{"value":{"entity-type":"item","numeric-id":832015,"id":"Q832015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6165889$7713108B-24F9-471F-A5B5-B44A6C135CB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"75c51fc34b1b317a7e03e3f5619e37da770cd338","datavalue":{"value":{"entity-type":"item","numeric-id":832016,"id":"Q832016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6165889$B4AC294D-DBD1-455D-91B7-47F95ADC2215","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4867eaa6b0909a04eef15563a783dcd84d88c7ea","datavalue":{"value":{"entity-type":"item","numeric-id":1784790,"id":"Q1784790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6165889$DEC0ABBC-6E0A-431B-96E3-F3012C02892A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6165889$4541E71E-41EC-4A20-A6A1-73AF3B869CC6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c377ab7875b781eda1304e6f4ef79ea097f76f82","datavalue":{"value":{"time":"+2023-08-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6165889$D553BFAA-B9B8-4EA7-BBE1-632CD1DE243C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6165889$967A99FD-FE80-4CA0-89A8-5717063409FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6165889$349A81CE-E683-4B55-A2FB-8823A693038D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3f07f94e9f92514883e35aa8078938aa77fe82ca","datavalue":{"value":"7721150","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6165889$BF372581-B4AB-4538-BA23-1B30F01D9D19","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":"Q6165889$499014F9-C020-470F-9C1E-126BD9A08E20","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"558811142f5e4730094a3c1b3522fe1cf319d4f0","datavalue":{"value":"https://doi.org/10.1007/978-3-030-03044-5_9","type":"string"},"datatype":"url"},"type":"statement","id":"Q6165889$51DBD89E-065A-4F36-97E3-DEC719BFE444","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9c0fd63131751d828bd6bf7deff965c84c68ae93","datavalue":{"value":"W2895822369","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6165889$A77D4F6C-5F5A-4C2C-8316-4F4B654BC040","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a6c270dc035825547c35d6bd73ac01bdfc061acd","datavalue":{"value":{"entity-type":"item","numeric-id":1784791,"id":"Q1784791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"563efdcfdac67a225e190601dfbb97312d76bd6d","datavalue":{"value":{"amount":"+0.7599455118179321","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":"Q6165889$8FC7976E-EDA8-4E6D-8CC4-1C47FE115930","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9bd71d433d357833a1ab35135bc0074a796311f9","datavalue":{"value":{"entity-type":"item","numeric-id":4414373,"id":"Q4414373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f00f9f7614f5787ecf58029fb72e0434a90fb782","datavalue":{"value":{"amount":"+0.7465726137161255","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":"Q6165889$D90AAB13-D9F0-472C-A1F8-37917085FFC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bccbf5fc3944a9c4a28f412cecb088c5b82edac0","datavalue":{"value":{"entity-type":"item","numeric-id":5900667,"id":"Q5900667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c51af809eec4572f143811c2e9886a89032a2b4c","datavalue":{"value":{"amount":"+0.7445070743560791","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":"Q6165889$4415F119-49ED-47C8-8C83-E95B194ED8CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ee785b8bf0751d66abea2867edda087f6ad28a43","datavalue":{"value":{"entity-type":"item","numeric-id":1680264,"id":"Q1680264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59df083d6a2ba1e9a34a71641efc5b0e33b5a629","datavalue":{"value":{"amount":"+0.7395328879356384","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":"Q6165889$60DB413E-F301-4F87-A427-A47410F0C3CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2b9fc369e46fc329463fea3bac110c1110bcfcc7","datavalue":{"value":{"entity-type":"item","numeric-id":5716541,"id":"Q5716541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0c3470b690aa241b59b56ec2d34f67e6e34b236","datavalue":{"value":{"amount":"+0.736802339553833","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":"Q6165889$7BE3AAFB-40D3-4384-B656-29CB899AAD40","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Constraint reusing and \\(k\\)-induction for three-valued bounded model checking","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Constraint_reusing_and_%5C(k%5C)-induction_for_three-valued_bounded_model_checking"}}}}}