{"entities":{"Q4612433":{"pageid":6642016,"ns":120,"title":"Item:Q4612433","lastrevid":82309313,"modified":"2026-05-06T20:35:49Z","type":"item","id":"Q4612433","labels":{"en":{"language":"en","value":"Accelerating LTL satisfiability checking by SAT solvers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7009547"}},"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":"Q4612433$CA679BCF-8622-4E1F-BF3D-1B800A301E30","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"27d9fc5368866349c0cf125c73c0e0e865e0e0cb","datavalue":{"value":{"text":"Accelerating LTL satisfiability checking by SAT solvers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4612433$F11B8D5A-63B7-4B59-A7E4-0ED24E30699C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5f883d0541c0d517a36e7c23d85b690f66fa2b73","datavalue":{"value":"1410.68235","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4612433$E02A72D4-9CAB-4CA2-91D5-0A59183F34D3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"82832e6ead7fd0129a06a766786f66a3d6aee0bc","datavalue":{"value":{"entity-type":"item","numeric-id":1707338,"id":"Q1707338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4612433$B88B2E4F-F344-4EBA-AA13-09081360B56B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6f8b1a64d507a032cda525aa6a0e7593e342c9a4","datavalue":{"value":{"entity-type":"item","numeric-id":1707340,"id":"Q1707340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4612433$7BC1F04E-C77E-4385-8000-A3EF08C1DA4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ce87cbb6ded942a7df2b71cd7e21808de8efe775","datavalue":{"value":{"entity-type":"item","numeric-id":208771,"id":"Q208771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4612433$08A52517-8BA8-40EC-8AB8-096B7A23374F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b8b4b706e0e1892c8640abf317cd4e1ff44c4fa9","datavalue":{"value":{"entity-type":"item","numeric-id":207989,"id":"Q207989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4612433$95F5DCD9-F18A-437B-95EC-BE7F8E12EE51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5894425868796c1c566a284833508f3ef0277bc9","datavalue":{"value":{"entity-type":"item","numeric-id":764615,"id":"Q764615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4612433$545C11F8-AD0F-46DD-A130-2BCB846E4803","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6cff588b238fe649ad35be9c49b1edf5332cb4aa","datavalue":{"value":{"time":"+2019-01-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4612433$3408D4B8-20EF-4FD8-AD12-33DD2AE4D606","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4612433$F42FC68A-3A01-4C45-8FD8-2413781806C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4612433$796C1A1F-11ED-4C3B-8AC8-9C878CBB1E6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4612433$C7F4B797-440E-4E1F-A842-39A056F5E153","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c8ca34b9163042a74ea7ba13450928cefc0b5e51","datavalue":{"value":"7009547","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4612433$EAB19AC5-2F3B-47DF-B9C3-1DD229180C79","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f1cf12c900aeb5813ce8f84db8812e6bb27ae87","datavalue":{"value":"linear temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4612433$7A0C1280-8419-44E4-A656-454339EA3EE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"07ff9f915faf2d9995f5624f4d84a4cd6126af6d","datavalue":{"value":"LTL satisfiability checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q4612433$776487F9-E2AA-4F3B-BA64-4BCF69FACB90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ddafeb91baec6080066b0cc9d71d2ad9f4a8dc9","datavalue":{"value":"SAT-based LTL satisfiability checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q4612433$BFB65E0C-9F4A-4395-9A64-23B1BFBDBC74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1b8f73aaf5b1ab0e7ed8b9832b9a7d5526183d22","datavalue":{"value":"obligation formula","type":"string"},"datatype":"string"},"type":"statement","id":"Q4612433$C6D509C6-A4B4-46D4-A752-6FF0EE6F5285","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2f8be496afa70f96c42c9d007ca2434d452e47a9","datavalue":{"value":"satisfiability checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q4612433$80F2C4BF-F785-4351-81EA-0E8F212A32AE","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":"Q4612433$88A5B60B-EC2B-4C16-A19E-1D703CEAA326","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3dbb4825e5529ffe8048c2bd3cccc5b0b041f589","datavalue":{"value":"https://doi.org/10.1093/logcom/exy013","type":"string"},"datatype":"url"},"type":"statement","id":"Q4612433$B20AE983-8454-489C-95D1-475DF09A7F5B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"260f0cef49db2a5a1a92dd6eab51473817f9e8de","datavalue":{"value":"W2796612952","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4612433$DECBE361-C01F-4E36-BC15-257A11723AAD","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"39975f57c878ca5acdba594ee83eb729aa06b19f","datavalue":{"value":"Q130117311","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4612433$369E2245-124A-4D21-85A8-CC4D64E204F9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bcc06774c3483e0a23b86e547f328223659a40e9","datavalue":{"value":"10.1093/LOGCOM/EXY013","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4612433$8ED6E33A-ADDA-4FC7-B3FA-3FC7A7E0C889","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"9e6aedf3faf6964e0bbb1663882629f007284aa9","datavalue":{"value":{"entity-type":"item","numeric-id":2983390,"id":"Q2983390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4612433$E468072D-1BA8-4925-9AAC-4A9817BD8CD9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a5e285b1a9095f370590c24f79161dd94db6b4d9","datavalue":{"value":{"entity-type":"item","numeric-id":2335900,"id":"Q2335900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"754c05792ae74cd2e84a76b74273b09c556890c1","datavalue":{"value":{"amount":"+0.84112548828125","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":"Q4612433$E90840A5-8B48-47E9-BD58-FC92A2F9898D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d55558c882eb537dea8b4ed637072d46a41d3d4c","datavalue":{"value":{"entity-type":"item","numeric-id":1707341,"id":"Q1707341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"69215bcab34a04b3cc1c47d85202882445838859","datavalue":{"value":{"amount":"+0.8367331624031067","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":"Q4612433$4DC1602E-9D6B-4B8B-807A-9B22728D0A10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dec1845d5b805a33a9b6dc48ef7a1a69c506e41c","datavalue":{"value":{"entity-type":"item","numeric-id":2046017,"id":"Q2046017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"796cd6dfa2472489b8a9136adebec089de797e27","datavalue":{"value":{"amount":"+0.8313525915145874","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":"Q4612433$D90EBE90-7CFB-41A1-AD4C-534E4E308094","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3383aee9a50302aa883ab2b30b18bea8e0a22854","datavalue":{"value":{"entity-type":"item","numeric-id":5283016,"id":"Q5283016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"314c7d6e94de79e24b42505e9e31d6b4bc523da7","datavalue":{"value":{"amount":"+0.8228779435157776","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":"Q4612433$19942E8D-9FAD-4380-80F9-A8856657322B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a523bc57602f5baeefda17c122f742e39fff24ac","datavalue":{"value":{"entity-type":"item","numeric-id":472802,"id":"Q472802"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e8e80e7929a5ad29837295a94b020821c32e3e6a","datavalue":{"value":{"amount":"+0.8035148978233337","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":"Q4612433$79702ADF-BD41-486B-8AF6-F0A4EFCE54FD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Accelerating LTL satisfiability checking by SAT solvers","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Accelerating_LTL_satisfiability_checking_by_SAT_solvers"}}}}}