{"entities":{"Q2891459":{"pageid":2902184,"ns":120,"title":"Item:Q2891459","lastrevid":51491423,"modified":"2026-01-18T11:59:27Z","type":"item","id":"Q2891459","labels":{"en":{"language":"en","value":"Automatic verification of TLA\\(^{ + }\\) proof obligations with SMT solvers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6046618"}},"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":"Q2891459$17DC822B-2DE7-4365-830D-D9E3E87976FF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ae49f6686cb20d38c592727028b1ac4b65890375","datavalue":{"value":{"text":"Automatic Verification of TLA\u2009+\u2009 Proof Obligations with SMT Solvers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2891459$033EE782-592D-4103-86AF-EB4353726025","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f44ca8e610b371c71a44206aff03d9b5d4971be0","datavalue":{"value":"1352.68159","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2891459$55ECB83F-9BEA-4091-BC51-C27E786DC8C0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d45fa20d06f9c4240042314abd4a8e0cff5eca33","datavalue":{"value":"10.1007/978-3-642-28717-6_23","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2891459$BBBF68CA-F4CE-498A-8F74-0FE524E4F40A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5a4b473513180cf93e4a8c86844a2c4dad9ce336","datavalue":{"value":{"entity-type":"item","numeric-id":820130,"id":"Q820130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2891459$DE68DC6C-1E88-4F24-BE9D-2F2A9AB36A91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4c8b99b92af834ae91a009c8d2943ce34df8c71e","datavalue":{"value":{"entity-type":"item","numeric-id":2891458,"id":"Q2891458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2891459$21163CF5-224B-46A8-A061-9BEE18DFB0EA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"23864e2be568bb8a6a4b0526f5a5216348320070","datavalue":{"value":{"entity-type":"item","numeric-id":2870110,"id":"Q2870110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2891459$D6D216F2-A657-4CF7-8193-186BB563DAE6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3e77e8a5f31c3c130201e11da285f79066a6e7f3","datavalue":{"value":{"time":"+2012-06-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2891459$575D3440-6F29-484E-B706-39D06100A95E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3ffdc5aad03cb1fd836566235ecefd14b82d68af","datavalue":{"value":"https://hal.inria.fr/hal-00760570/file/tla2smt.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q2891459$7639C092-4DF6-4453-974F-A4F947EE2266","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2891459$D77C2ADA-C25D-4B1E-8B3D-3A45E46850F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2891459$D9D5FE3F-D916-43C5-903D-C1F9B4861B20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2891459$633B89E1-E43B-41C7-9C3A-4EF28E3168F7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7f42040dd18a5abc224830722b8f7d718f4d151a","datavalue":{"value":"6046618","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2891459$3623E8AD-24B3-44CE-BEB5-37317330B782","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"85575b60ef4d0a8413d3c895be2530b8915bc3fb","datavalue":{"value":{"entity-type":"item","numeric-id":16612,"id":"Q16612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2891459$06FCAE0E-CC92-4AAC-BFCD-65A587036399","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2891459$8BE357B4-2793-4C9C-8ACB-904326A72F14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2891459$52F6C948-11A1-45BD-B279-59139F680CB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e3fa1be4925f6565903e34254fe3ce3cb99beabc","datavalue":{"value":{"entity-type":"item","numeric-id":18828,"id":"Q18828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2891459$9472F40C-AFA0-4CC4-8374-1242C431A136","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9b0860d94af5fdff4b5635709ae334aacdf07ca1","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2891459$11279518-2760-4A32-B5A8-D9A23FC1F8FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6635cd024ea0b7601d03e4b2d3631551a4364421","datavalue":{"value":{"entity-type":"item","numeric-id":21509,"id":"Q21509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2891459$1B8EC3CC-3B6A-4E5E-AECA-D994D4FF2DFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6d1b503d7c8f19634e207574177819c306621855","datavalue":{"value":{"entity-type":"item","numeric-id":17038,"id":"Q17038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2891459$62B6FB97-6070-4290-8B84-674BFEC4C8DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2891459$E0D34AFC-1F3C-4565-A3B9-3649C639E0E8","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":"Q2891459$ACAA95DB-447B-474A-AAC6-9B39D765791D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1ad2109085c5f14629ab4e6116ea5f660c3d5236","datavalue":{"value":"W29617856","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2891459$53778FAE-9A96-4310-8138-F9AC2596F4C9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"383293963e7c1b01bd5a14b4cc3c73537c26a169","datavalue":{"value":{"entity-type":"item","numeric-id":4647839,"id":"Q4647839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4bfe2f3c98837ad771d404aaf34f1edd70522d00","datavalue":{"value":{"amount":"+0.8205032348632812","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":"Q2891459$51E66F39-C8B7-456B-8356-D169793F8A7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7f5338f7ed3775f2c4b0a5afeaf8ce6094c68557","datavalue":{"value":{"entity-type":"item","numeric-id":3024875,"id":"Q3024875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"89b5077a9223c5a8d57089913c810284cbc04664","datavalue":{"value":{"amount":"+0.7465104460716248","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":"Q2891459$2CEB77A4-3BA7-4C7C-8CDE-4C7954B1DBCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a35dc3289e2432f10ae8b38ca7b9fb5a59f2610b","datavalue":{"value":{"entity-type":"item","numeric-id":5881447,"id":"Q5881447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d4a4279f126e22ca403bb6719b23b9790c5a0d0","datavalue":{"value":{"amount":"+0.7436124086380005","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":"Q2891459$5F478B81-C640-4D28-9084-0502709D6467","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"58d47caa41a11da514de99ed10b7d55ea0610de8","datavalue":{"value":{"entity-type":"item","numeric-id":4934623,"id":"Q4934623"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2a10d8aac9fd143ac7bbefe495c3d9a36ae6a592","datavalue":{"value":{"amount":"+0.7381287813186646","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":"Q2891459$E3FDE799-396D-4D8B-94C1-0F64040C73C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b56c2663181216be8ba0e60dbf3635b9c0d91124","datavalue":{"value":{"entity-type":"item","numeric-id":4494386,"id":"Q4494386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2a10d8aac9fd143ac7bbefe495c3d9a36ae6a592","datavalue":{"value":{"amount":"+0.7381287813186646","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":"Q2891459$CC5F7227-6A5F-4B98-A043-066D2A3F3BC0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2891459","badges":[]}}}}}