{"entities":{"Q5900667":{"pageid":8006748,"ns":120,"title":"Item:Q5900667","lastrevid":50958383,"modified":"2026-01-15T22:39:47Z","type":"item","id":"Q5900667","labels":{"en":{"language":"en","value":"Bounded model checking and induction: From refutation to verification (extended abstract, Category A)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5695346"}},"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":"Q5900667$80CBC94A-FFE3-4387-BA9D-0F522F1456AB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"73bd069b212797cd1b716ecedbde3c2b856d1f40","datavalue":{"value":{"text":"Computer Aided Verification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5900667$83247033-7D97-403D-BCDE-E2E29ABA518A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"fa04040c97d471990f75bfb70fba77d76496470c","datavalue":{"value":"1278.68199","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900667$4554C23F-0F96-42B0-ADAA-4662831B66EB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"899468d0fe4ec0ae9c5ef91b63881ae72bf40a46","datavalue":{"value":{"entity-type":"item","numeric-id":438532,"id":"Q438532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900667$652C1BD5-5BD8-4394-AD24-5404A539CC71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"69e260a263a8c533b05d7f8d3aa8c89b45a7453f","datavalue":{"value":{"entity-type":"item","numeric-id":2055858,"id":"Q2055858"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900667$508BFC5C-48C4-41F1-B276-34266E33C7FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"00f475b4fdf76b005bc72fe14b40c387d4b0206c","datavalue":{"value":{"entity-type":"item","numeric-id":2842587,"id":"Q2842587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900667$835F730E-04CB-456B-A071-6EFFA7B78345","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":"Q5900667$ACCE14FF-3D23-4824-A42A-56D9B8A98893","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2c61bb6d282cc95675f5b726985d020f8b0e6f23","datavalue":{"value":{"time":"+2010-04-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5900667$01693A62-CD61-4AC2-9B5B-550FCD7F0C03","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900667$434037D3-2A98-44F7-8960-40D1D83CF756","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"176e47af9f9e7cf4ebff07fc1f9e4f94a83134c1","datavalue":{"value":"03C10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900667$7666565E-6084-48F6-A8F6-6B047BB9BFE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9b78776a56fc28cdd893baa47605a105412b838a","datavalue":{"value":"68Q45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900667$6FE6189B-AA88-4C4D-8B9A-66D2E124CDAA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1c34615a0874dad745d81c6c130eee02a0b3114f","datavalue":{"value":"5695346","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900667$3048CF48-F053-4646-953B-3A6C628BAE2A","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":"Q5900667$83C0E42B-97BF-427B-8097-4EB58B2DE724","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"050caeb9facfc2b37142c301b40d1dfd9dbf1be9","datavalue":{"value":"https://doi.org/10.1007/b11831","type":"string"},"datatype":"url"},"type":"statement","id":"Q5900667$B844F813-7EF7-495B-A9F9-61B42AA1F083","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ca9b9df0d9ff4e5d8e3d66da51426dae32b7ea5b","datavalue":{"value":"W1571340194","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900667$501E4CA0-E2AD-4A5A-8FCD-EE719DED921C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0bc3be280ea47ce2c61f3b7e2b376b1d1ce60a5c","datavalue":{"value":"10.1007/B11831","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900667$46A89B9B-B919-4A37-8DC2-F5277945AA31","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04bdf0742bdd522dee8d4e004977de201c067fa6","datavalue":{"value":{"entity-type":"item","numeric-id":2369883,"id":"Q2369883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"acd4d46513ad4e7be26f574b2a29eb67715570ed","datavalue":{"value":{"amount":"+0.8283738493919373","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":"Q5900667$13D26D3E-F692-4267-B214-BC9587E0CDA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d4be7d7978e80bb59263872b297862b5cb916f8","datavalue":{"value":{"entity-type":"item","numeric-id":4809077,"id":"Q4809077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"15cd4e5dd0650249bf0b814db9babd51af517488","datavalue":{"value":{"amount":"+0.7941935658454895","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":"Q5900667$D6463704-5D79-4FB1-9EBC-BDF9961CBDC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9140f24107c22d73c2cfc5e16679a500cd14994c","datavalue":{"value":{"entity-type":"item","numeric-id":2044196,"id":"Q2044196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"51da9db8d432a37f575f29b7d0aec16503e8b091","datavalue":{"value":{"amount":"+0.7899960279464722","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":"Q5900667$F0952FDD-ABBB-4786-9DF0-60465F3E161A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"417f3b972ebf403c2e595613f41ecaa318eb253e","datavalue":{"value":{"entity-type":"item","numeric-id":1878909,"id":"Q1878909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"076f31010107f95e7645a3dc676be3af29dc322a","datavalue":{"value":{"amount":"+0.7757875919342041","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":"Q5900667$72619710-FAD2-4B57-BC97-72A93FB97B57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"97a1bf693cef9178aadd375963cd412c8809cc24","datavalue":{"value":{"entity-type":"item","numeric-id":3176368,"id":"Q3176368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"801f44504d3b89513759ce6860349664dc8c37fd","datavalue":{"value":{"amount":"+0.7584223747253418","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":"Q5900667$DAB42014-126D-49E9-9A7D-237FDF976EEA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5900667","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5900667"}}}}}