{"entities":{"Q2046017":{"pageid":2056759,"ns":120,"title":"Item:Q2046017","lastrevid":57696762,"modified":"2026-03-31T22:59:11Z","type":"item","id":"Q2046017","labels":{"en":{"language":"en","value":"SAT-based explicit \\(\\mathsf{LTL}_f\\) satisfiability checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7382223"}},"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":"Q2046017$6B4E4D8C-1383-4174-AC79-1BAF915FE80F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5260dfb4b50cbcb1cbce0174ffa751f4bda7a0ff","datavalue":{"value":{"text":"SAT-based explicit \\(\\mathsf{LTL}_f\\) satisfiability checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2046017$F91697BE-DDDC-431F-BF53-07BFA556D835","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"281d6ee9d3ea099f03c7f8ba9c868cccc5b4ea5d","datavalue":{"value":"1504.68205","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2046017$EA4DB685-0EF5-4485-9724-44AF322E7D58","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":"Q2046017$B8634A50-3567-4CC5-91A7-C5AB8D982734","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":"Q2046017$EBBEC678-2B22-4ED9-84AA-F9662DD18E17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f0be3906e1e89d082fa47b421fae0cc089eff023","datavalue":{"value":{"entity-type":"item","numeric-id":2046016,"id":"Q2046016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$69EED446-E49E-49C1-97F4-2B98A3CB8B1C","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":"Q2046017$1E0DD967-2D47-4463-981D-673BA1CE7714","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"63732236fa66d5c3f9fb2c4a703259d2ca600fe1","datavalue":{"value":{"entity-type":"item","numeric-id":1996029,"id":"Q1996029"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$93CFF645-AB87-4A37-8210-23C7B9128442","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"984e6510ec40a363d20e607cce2cc2f8b07918ae","datavalue":{"value":{"entity-type":"item","numeric-id":72340,"id":"Q72340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$0EF9F3FE-0033-4FB0-872A-62CCD79D82D3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"509f91048bfebeb2e3809071f1ccdd7172b43404","datavalue":{"value":{"time":"+2021-08-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2046017$3FF3A504-C319-4F13-AB1F-359274D07450","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d61ea6ba7fdabdf14819932ed328f241e37cb90c","datavalue":{"value":"https://arxiv.org/abs/1811.03176","type":"string"},"datatype":"url"},"type":"statement","id":"Q2046017$0FB12D23-6719-4968-9701-C50A892EB33D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2046017$CA9097E9-6335-4B11-80BF-AEAB86FCB683","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2046017$C1E9CF77-207E-4329-911D-09FEFC5EF767","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e3acd076c87f5906b9d69e23b1e206925d38a993","datavalue":{"value":"7382223","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2046017$9D5C8574-E671-4A88-85B3-BB1C7E7A9545","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7d57bb144619d868488ea7e6a0e0e5eeeb254d2f","datavalue":{"value":"LTL over finite traces","type":"string"},"datatype":"string"},"type":"statement","id":"Q2046017$60CE3760-413C-4775-AEAF-53065499F24C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2f8be496afa70f96c42c9d007ca2434d452e47a9","datavalue":{"value":"satisfiability checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q2046017$0909100A-50AC-4184-93A5-7975256B25C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6c20f9d2d0f6abfb4a980b10a35230a11406dbf","datavalue":{"value":"SAT-based satisfiability checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q2046017$68E4ABEB-71A5-4DEC-A7A1-119F51D854F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8f6c84d84bf44b3897f104ba73fbfcc1e8ee39f1","datavalue":{"value":"conflict-driven satisfiability checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q2046017$C8B8536C-3E88-4964-A88D-748E4CAF21B8","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8449db7d9aaa28101ba7b0de8e98d9c446365070","datavalue":{"value":{"entity-type":"item","numeric-id":13332,"id":"Q13332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$5910D5E4-2708-499A-9478-95BE1152DA02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a4e1fe9e7e19a9673e889bcce0afc1d800822389","datavalue":{"value":{"entity-type":"item","numeric-id":30365,"id":"Q30365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$A0C9AAE9-8975-4375-8824-15863ACC6172","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3635e00f6ae941332a023c33e377503df2343121","datavalue":{"value":{"entity-type":"item","numeric-id":32502,"id":"Q32502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$5940F224-0926-46D0-99D4-19EA22E4F616","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":"Q2046017$500F0EE3-6350-47F6-BC2D-052E892DFDA4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"75d2a9a8018c20cce0a99b241ea8c780ec90f4e6","datavalue":{"value":"W3064086008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2046017$A2D95417-4D7D-4BF2-87D6-2739C46E571F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"03455b971397d937afa50b2acf41cc84429c8a88","datavalue":{"value":{"entity-type":"item","numeric-id":465680,"id":"Q465680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$F2B5C207-75CB-4DB0-A929-E9B2321CA46E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6571f5e7b59314ce70c60fe99520c2ad4472991","datavalue":{"value":{"entity-type":"item","numeric-id":5452603,"id":"Q5452603"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$AA2AC056-15D9-4418-86B0-7C9A2829C082","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5955d3e0fd0050b5f260736db49efaa72acd0df1","datavalue":{"value":{"entity-type":"item","numeric-id":6041134,"id":"Q6041134"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$34381537-CF1E-4F10-BB32-1879316A835A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e10b94faed1369f0d6cedaf8543971a89c594ce","datavalue":{"value":{"entity-type":"item","numeric-id":5900668,"id":"Q5900668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$3B354262-850B-42F8-9710-7278D88D6AF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"692f33298e12548a7de121e9b379ab5a875cd0fd","datavalue":{"value":{"entity-type":"item","numeric-id":1383350,"id":"Q1383350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$087C303D-7725-488D-A8E2-276803914421","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ce585837a919025fa0560b9c65a92d28da1c713","datavalue":{"value":{"entity-type":"item","numeric-id":1978242,"id":"Q1978242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$8C46192B-9369-4F65-89EB-0F5749E53F96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"74e8845ea20c22b9539eb5d3a836d23aeea68d73","datavalue":{"value":{"entity-type":"item","numeric-id":646542,"id":"Q646542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$19E7833B-9DCA-44C3-81A9-A2882B5096BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef9a85754f10c794d7ea794155cce4bd2f066956","datavalue":{"value":{"entity-type":"item","numeric-id":3075471,"id":"Q3075471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$04E22B34-66CC-4A34-9DF5-D3CAB4C7ED4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"212915fd370f63215c162b6371370a744ceeadf1","datavalue":{"value":{"entity-type":"item","numeric-id":5429344,"id":"Q5429344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$91ED8950-ECE1-49A5-B5D8-DB926599F948","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22485e2e7f5d751287059d6c89f8749b6a408a20","datavalue":{"value":{"entity-type":"item","numeric-id":5325885,"id":"Q5325885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$F85EB373-A93F-42C6-B594-C4F64DA2108B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dbdbc7a9071875aac437c4544c1a225a570a3964","datavalue":{"value":{"entity-type":"item","numeric-id":2324218,"id":"Q2324218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$BD76B56D-86FC-414D-83B5-85BF92DCA691","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a09c83e127b33f2b447a249abab694bb8942e1cd","datavalue":{"value":{"entity-type":"item","numeric-id":4558796,"id":"Q4558796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$6B425B7D-4439-4474-9486-76B76D3D56A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64052bf66d4808ae98a3365915a7f430a9951822","datavalue":{"value":{"entity-type":"item","numeric-id":5899036,"id":"Q5899036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2046017$4D3F14C5-79F9-49AF-A79E-5C054E698C5F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"45f3f8e5653695a3993df06533915b9917323a4f","datavalue":{"value":"10.1016/J.ARTINT.2020.103369","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2046017$CC009080-0A32-42D5-A13A-8D6EBCD68BC0","rank":"normal"}],"P1643":[{"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":"c516fe3ef16cc5a561caf2db1d9350f9dac682dc","datavalue":{"value":{"amount":"+0.879034698009491","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":"Q2046017$9712A6F6-7AA1-4D27-A4B8-83D3FEE1CE89","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":"d0f5e0083c91b6975522be2cc21b2d97cd174f3c","datavalue":{"value":{"amount":"+0.854323148727417","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":"Q2046017$CD5D206A-EB52-474C-9EBA-357DAA5204EF","rank":"normal"},{"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":"098d7118a2bf4035084e12e93c76c71c5f3b9471","datavalue":{"value":{"amount":"+0.8536931872367859","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":"Q2046017$09BE1E1B-ECBD-4A70-96AA-324BCD6CAD6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c99efe65a80694c2247f8810e011b1b26faef365","datavalue":{"value":{"entity-type":"item","numeric-id":4612433,"id":"Q4612433"},"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":"Q2046017$CE810521-0035-4BC6-8E8D-BD0835F60FAC","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":"722f0bbd1d48b421b04dde19b9cd1d26148043f5","datavalue":{"value":{"amount":"+0.7937143445014954","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":"Q2046017$0331F212-0EE2-47EB-8D28-517FE991CB3D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2046017","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2046017"}}}}}