{"entities":{"Q5758121":{"pageid":7787672,"ns":120,"title":"Item:Q5758121","lastrevid":97356812,"modified":"2026-06-05T14:32:03Z","type":"item","id":"Q5758121","labels":{"en":{"language":"en","value":"Combining Abstraction Refinement and SAT-Based Model Checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5185790"}},"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":"Q5758121$DE630B75-E1F9-4EE0-A1A7-28FA029CAF7C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1caa003235bebc4d6821772c95f8a0c64a825c42","datavalue":{"value":{"text":"Combining Abstraction Refinement and SAT-Based Model Checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5758121$ED4AC58C-0765-4240-A0FF-3ACB54A3A9F3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4d48979ff058e09b30d6efc30af881ca6570f22b","datavalue":{"value":"1186.68274","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5758121$7DF9A560-1CA1-4670-9B29-A6F85B09A6AB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c1a8a21874885aa11bd48c4649ea0eac2df87ee0","datavalue":{"value":"10.1007/978-3-540-71209-1_31","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5758121$9788195B-1DE8-4421-9775-B1FCEEF5B7B3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"84c459dfa3e126377d1f2c022e5e3e523bfdfd61","datavalue":{"value":{"entity-type":"item","numeric-id":2769608,"id":"Q2769608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758121$2AB52A19-682F-42C8-8E64-E630FF64FC27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"57a84b3343ed70002617a9eb1439c18c15bac9ff","datavalue":{"value":{"entity-type":"item","numeric-id":934708,"id":"Q934708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758121$B960BE65-B531-4E1F-B1AA-630B13E3DB17","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":"Q5758121$E2B77808-E0FF-4033-A303-CCBC519F171B","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":"Q5758121$BC06A174-EA22-4EEF-B012-8F263C56D156","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5758121$A8E0FF0B-9D38-4B0C-BDD7-10E5AE139BFD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ce646660bcd2e8ecd9fcd8a0b8007689e2ae0bc0","datavalue":{"value":"5185790","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5758121$B2BF308C-5C7B-4CBE-82FE-592B5EBAB051","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"68889b620f959d2410d5024f9adee923736e93c3","datavalue":{"value":{"entity-type":"item","numeric-id":16818,"id":"Q16818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758121$B49AB645-E0A7-4CA9-B571-56966F42DB3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"478f9061f14e098e3fdf3fe3667d3a7084c42e61","datavalue":{"value":{"entity-type":"item","numeric-id":18982,"id":"Q18982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5758121$28648D2D-68A8-45B2-A56A-AE1A621FE77E","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":"Q5758121$5CDD77F3-529F-4146-97D3-C726DD3AE7A3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"67a6f3e7132dc719e80d6fee1b735df1d4c603bb","datavalue":{"value":"https://doi.org/10.1007/978-3-540-71209-1_31","type":"string"},"datatype":"url"},"type":"statement","id":"Q5758121$C775EB63-CF5A-4700-9520-063AF289CE2B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"be0bfcb85e0749537fe428e24e706d6571be6cf6","datavalue":{"value":"W1585696877","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5758121$6824F7AE-F343-477F-83E4-3FE7C5A84F5E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f3e4418b90254da47f1e3ab57975e595d219a0be","datavalue":{"value":{"entity-type":"item","numeric-id":5899061,"id":"Q5899061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4ed4906f6aec1b68c9ec03bda6dc4dac0de25ef2","datavalue":{"value":{"amount":"+0.8736017942428589","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":"Q5758121$60B237D2-B81A-49C0-B6AD-DABED3A484D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0dbb9ce060d55e1b403f2129112efe14249c6bae","datavalue":{"value":{"entity-type":"item","numeric-id":2845512,"id":"Q2845512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b0f84994188691588a218510f9da2385ff355b5b","datavalue":{"value":{"amount":"+0.8515638113021851","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":"Q5758121$8002103E-CA04-4795-84C0-B6A1FA141C41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d45dd440df75f6c635ba254138a56ee3d488dded","datavalue":{"value":{"entity-type":"item","numeric-id":5900666,"id":"Q5900666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bd0119afa3c71001f5c7f81a89d5435eb02b72f6","datavalue":{"value":{"amount":"+0.8236871361732483","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":"Q5758121$179807F4-CC1A-41B4-9EBE-FC5F1CA33158","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bd40460bef7592e9f11c579ff25795b0835cbe7c","datavalue":{"value":{"entity-type":"item","numeric-id":4417909,"id":"Q4417909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0431cf730144bab8e7fbc5f604f7363cb37e99ed","datavalue":{"value":{"amount":"+0.8183237910270691","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":"Q5758121$2475EB73-9628-4EF7-95F2-91CB3D263C23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aaa75d14f411a29ded225a875d13f512a1857ea9","datavalue":{"value":{"entity-type":"item","numeric-id":4427894,"id":"Q4427894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d3372c0e89a732e70d3b00419f83d6bf625f121b","datavalue":{"value":{"amount":"+0.8119125962257385","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":"Q5758121$9423852A-D2B8-4FB2-9F6C-BE98E73432BE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Combining Abstraction Refinement and SAT-Based Model Checking","badges":[]}}}}}