{"entities":{"Q2864381":{"pageid":2875101,"ns":120,"title":"Item:Q2864381","lastrevid":51886607,"modified":"2026-01-20T11:42:35Z","type":"item","id":"Q2864381","labels":{"en":{"language":"en","value":"A compact linear translation for bounded model checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6236391"}},"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":"Q2864381$3550166F-E1D9-457B-9A1C-3C31EB9D229C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"97b845a3924a7c19d6fa81f0ed040ab9b8310664","datavalue":{"value":"1277.68134","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864381$3DAFEB69-6CC2-47A2-B7DD-978E4C125D94","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"849271e65f86db683897e2dc0e43d66cba64f6ce","datavalue":{"value":{"entity-type":"item","numeric-id":2331076,"id":"Q2331076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864381$32EAD8EA-C5A9-4359-A81F-B72FE7EB7C3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"eea7ba02ba8f253abb4f4e9c8bf03b50404902f7","datavalue":{"value":{"entity-type":"item","numeric-id":2849597,"id":"Q2849597"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864381$684ABE1C-7531-460A-98E1-F508C4610998","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864381$67CE2E79-27D0-4304-8956-68C419CE10D7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"deb6cb3450bd256fc635dc32234471403070c2b7","datavalue":{"value":{"time":"+2013-12-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2864381$5E1DFA7A-B23E-4CC5-B1B7-3E11A96FB45A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864381$416F08CF-649B-476B-809E-8AE7395EED6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864381$1761CBB5-D365-49C5-A8CD-CC4080D3D37B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"142fecbf6d55b0828ec31e306b4d757ee388fa6a","datavalue":{"value":"6236391","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864381$D40C8178-40E0-477D-B1D1-953F5614C53F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6ab41959fd9494b5548d09c762ca90a9336e1c7","datavalue":{"value":"bounded model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864381$2DFE63C5-E8EA-40D7-BD08-AA5CC5EF237E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f1cf12c900aeb5813ce8f84db8812e6bb27ae87","datavalue":{"value":"linear temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864381$1817BDD4-6C11-4410-BE68-5B17609977B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"58f5b38fb2a74b9d769b35f0082d509945130efd","datavalue":{"value":"fixpoints","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864381$6266472E-0BF7-42E6-A083-948031BC7773","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5867ec7b44aefc01672736513dfe6410a0300cd5","datavalue":{"value":"SAT","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864381$EA7EB735-DD8A-46DF-840B-F62727418BA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"51802126f63d5102d578f2858428d5d0f09da73b","datavalue":{"value":"denotational semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864381$1A33DC79-A19B-469D-928E-70F7D29BF2D0","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":"Q2864381$17791EE4-76B3-4F8F-BA4E-05AC1F5FC4D6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d804819c5d1dbddd8d945f562e3e771c2050f8a8","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2006.12.020","type":"string"},"datatype":"url"},"type":"statement","id":"Q2864381$D4E345ED-95BB-4A24-A818-6F1FD1C3ED86","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2b00deb40b7ef918f2085560273d9202f88a49b8","datavalue":{"value":"W2148461683","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864381$6A8A4D12-0AFD-4618-A979-E1B8D11B9E6A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c0e430ac953987f7ace9d78fa87f21f8cf10d86c","datavalue":{"value":{"entity-type":"item","numeric-id":5492984,"id":"Q5492984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864381$EB141DC3-7C5E-4D5D-8CB0-1EDE49F83EB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5b330f5cd7a65a8735b5cd88f9d99cd7626efdb5","datavalue":{"value":{"entity-type":"item","numeric-id":4012170,"id":"Q4012170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864381$34353F64-0742-4C4F-8EB1-929A45484689","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26b33d870b8b658fa2258573b1c239cb2fe2b4b5","datavalue":{"value":{"entity-type":"item","numeric-id":4427907,"id":"Q4427907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864381$AEF33652-98CD-4492-9D2C-5E9B21FFA20C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7f5f3cd0c0fdd70d2eae3e5f69e2ee0aa687d8a4","datavalue":{"value":{"entity-type":"item","numeric-id":5716540,"id":"Q5716540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864381$2CF59025-CB8E-4078-81F7-18A6EC624D5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"521fcf11de7d8721521e1e478560508699e8a82f","datavalue":{"value":{"entity-type":"item","numeric-id":5492980,"id":"Q5492980"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864381$5DE600AF-0E96-4D2E-9206-053FA2198A9D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"31f3422aab03e00a71f7fb69ee5229355a24d73b","datavalue":{"value":"10.1016/J.ENTCS.2006.12.020","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864381$D48B32FA-AEF9-416D-9C33-78F6527CF404","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e17cfb4078f548990432b7ebf8c51216593dae39","datavalue":{"value":{"text":"A compact linear translation for bounded model checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2864381$FB7B2A53-EFEF-452F-805D-BD43F24E5D2D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"67f436796ae869c7866cb24a7b8262c489995b6e","datavalue":{"value":{"entity-type":"item","numeric-id":5492980,"id":"Q5492980"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4adc08dd181df76e80293fa691851792a5c05649","datavalue":{"value":{"amount":"+0.8656294941902161","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":"Q2864381$713B7E02-A299-4265-A931-12D71D651D60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4cd3d41e83c5b8c36bb26f88ebcbd122fd1d3af1","datavalue":{"value":{"entity-type":"item","numeric-id":3608783,"id":"Q3608783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a147717dd22d8748ba9adb2406748bab8cd4422e","datavalue":{"value":{"amount":"+0.8189168572425842","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":"Q2864381$12A7E1C5-224A-4A0D-8C16-ECF2B4667F5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4d8b7bc506570e1ffa0717751930e8078f520df1","datavalue":{"value":{"entity-type":"item","numeric-id":5310676,"id":"Q5310676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0d15db78597cf36834658eae3323b529f1b63364","datavalue":{"value":{"amount":"+0.8153480887413025","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":"Q2864381$39440F31-CF84-4C03-84D6-90F32A31F45C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"995e7a95a19a897b6da47f87a3b2152a0392b81a","datavalue":{"value":{"entity-type":"item","numeric-id":4427907,"id":"Q4427907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"30c19e9ac6392af0e68a995c8a334aee2cf3e99d","datavalue":{"value":{"amount":"+0.808404266834259","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":"Q2864381$58C12D8A-452D-4836-B405-C515EFDD68F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"825c9aaa727f79c201debbf710b791dcfdd806b0","datavalue":{"value":{"entity-type":"item","numeric-id":4736997,"id":"Q4736997"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"66e09f99d9bcd58ef87b5e843f7b115834878aeb","datavalue":{"value":{"amount":"+0.794294536113739","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":"Q2864381$0B534919-08DB-481E-80A7-2D04BB1F58E1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2864381","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2864381"}}}}}