{"entities":{"Q5946344":{"pageid":8123146,"ns":120,"title":"Item:Q5946344","lastrevid":47686264,"modified":"2026-01-02T10:38:49Z","type":"item","id":"Q5946344","labels":{"en":{"language":"en","value":"Bounded model checking using satisfiability solving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1658696"}},"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":"Q5946344$94B96D82-3C8D-47E6-96DC-7A1B0E268162","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c535175f332e0e273f95590866cf331664744342","datavalue":{"value":{"text":"Bounded model checking using satisfiability solving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5946344$717BD0BF-5D09-4C43-B04B-5930B58B9BCF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8980bb6ae235b1555731551202ab694d3c96f728","datavalue":{"value":"0985.68038","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5946344$92022E90-8F2A-45AB-B341-2BCECA99195E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d3b20616c0c26e4ead3045256c0496d3b461f613","datavalue":{"value":"10.1023/A:1011276507260","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5946344$F4F98A2D-51D7-4CD4-A8F2-11CB769EB3BF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4e4e5ed72bee66087d415d4f69d49eefd101a453","datavalue":{"value":{"entity-type":"item","numeric-id":526749,"id":"Q526749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5946344$758D13A2-D547-45D2-BDD0-026FA3EB3C17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"396db362b8f5a55e9aac7b42eacb07e40796d942","datavalue":{"value":{"entity-type":"item","numeric-id":209458,"id":"Q209458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5946344$B734C245-E622-4BC2-8C8B-C1039BC3DB55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"00f38b1ca4cfdd6ea7e531d633726995645477de","datavalue":{"value":{"entity-type":"item","numeric-id":209459,"id":"Q209459"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5946344$1E4F273D-0BB5-4EB7-998C-0C82632A34D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"971025d2b8fca86b0f7c7b3b9d5e348f38a2f014","datavalue":{"value":{"entity-type":"item","numeric-id":209460,"id":"Q209460"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5946344$69324400-051D-4844-B5CA-1348E991E73C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70551fcc6e89042fc26ae9242a005533b44a2d7a","datavalue":{"value":{"entity-type":"item","numeric-id":169908,"id":"Q169908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5946344$024736F1-BD56-4759-898F-DFE2AAC81667","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"cda08edf6e14c28a948f9b78f5bc4351bb49e6b0","datavalue":{"value":{"time":"+2002-05-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5946344$D177BE5E-6DAA-4B75-87E8-56D3DFEDA52F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5946344$062F54CD-C971-4D77-BF0A-25FF2929A6D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9b78776a56fc28cdd893baa47605a105412b838a","datavalue":{"value":"68Q45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5946344$F811AA7D-F263-4A23-84DB-973CFDBF74EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5946344$A71D05A0-DFA9-48F8-81EC-AEB0895A1C64","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cfffe423b6b9d6684f54fca8dd14a02a935ecab9","datavalue":{"value":"1658696","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5946344$1D65B23A-ACEA-4595-9A81-46E6526250C0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q5946344$32CA57A5-6F82-4B2F-923B-D75D198A17D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d9408546ecb33d5fe54dbb1dbe82b7a513b60f62","datavalue":{"value":"transition system","type":"string"},"datatype":"string"},"type":"statement","id":"Q5946344$82790A61-72FB-4BF0-B14E-5F1B7BB9E84A","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"7f9d024e470ba9c006cf3c93c272da7293677440","datavalue":{"value":"Q55889278","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5946344$96C5B8D8-0B3C-46F7-BDFE-0662AA94CF53","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f078e243cc5b2a268355ae913e6ed1ca3bb0dc8","datavalue":{"value":{"entity-type":"item","numeric-id":20519,"id":"Q20519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5946344$F80D409D-A4E8-4594-B4D2-D6CF56915D52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5834864074172f90c0db592b61fbce75f9303a03","datavalue":{"value":{"entity-type":"item","numeric-id":16627,"id":"Q16627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5946344$53DD94C8-41F1-4E32-8641-9A4376B3F701","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2a216d6c09dac0df49b00b19ed2bb5c4336ef7f4","datavalue":{"value":{"entity-type":"item","numeric-id":20231,"id":"Q20231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5946344$734BAE33-819C-4336-BE87-D33BCEAE17C9","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":"Q5946344$5DA7F16D-6EF6-46A9-A6D3-A2BBD0480F89","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f535e7fada6b0e4f2d88aec76ac57f56ce0ef515","datavalue":{"value":"https://doi.org/10.1023/a:1011276507260","type":"string"},"datatype":"url"},"type":"statement","id":"Q5946344$6EA631A7-36FE-4FB3-B84E-6DDDADD312CA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ef1efaaea72d6b1b5ac62bd8ae8618b78206afad","datavalue":{"value":"W1819209966","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5946344$8563C75C-EB7B-4BE3-996F-CA0259B4D059","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"0a0e5ef2c625f1317497d20817aa6ed9379739a0","datavalue":{"value":"journals/fmsd/ClarkeBRZ01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5946344$62D6237F-4947-4C83-AACE-E7BFC5382E83","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c05564e307a5083a6c81d193eb316b1f80be51ff","datavalue":{"value":{"entity-type":"item","numeric-id":5493231,"id":"Q5493231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d7fbfc6df52f3e5d054219529c7f3ffd58fc2cc","datavalue":{"value":{"amount":"+0.8826776742935181","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":"Q5946344$7CA54F8B-2CC7-4743-8D43-394A6BBC1B37","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":"7886e96c4ec7b2b6e6105251d8489362255ce220","datavalue":{"value":{"amount":"+0.8615661859512329","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":"Q5946344$4202CE9A-7E1B-440D-806C-819537C9DB60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4c63986bc7877fd690d0d55e152223739c1cf2a5","datavalue":{"value":{"entity-type":"item","numeric-id":3527691,"id":"Q3527691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0a70b995451b12f8ea5d646a78e8103737cb89ce","datavalue":{"value":{"amount":"+0.8614583611488342","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":"Q5946344$8FD41223-182F-427F-82F5-499DD0D1419A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0337eec65669bdb027f080d3087ed0d70cc9320d","datavalue":{"value":{"entity-type":"item","numeric-id":4738483,"id":"Q4738483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ab430898e6116210efd149e79baeec9a0a1c1033","datavalue":{"value":{"amount":"+0.8573561906814575","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":"Q5946344$B5702232-1F22-4D1D-9F02-59BC8B4D815A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6163a7aa78d81cf3b8065a62f631a6a5857595d0","datavalue":{"value":{"entity-type":"item","numeric-id":2754108,"id":"Q2754108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f64db415d0360557b5454b5228e266ec09867220","datavalue":{"value":{"amount":"+0.8543322682380676","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":"Q5946344$278EDBDA-F786-4583-925D-B2AC78DD83DB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5946344","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5946344"}}}}}