{"entities":{"Q4647839":{"pageid":6677420,"ns":120,"title":"Item:Q4647839","lastrevid":97959236,"modified":"2026-06-05T15:55:18Z","type":"item","id":"Q4647839","labels":{"en":{"language":"en","value":"TLA\u2009+\u2009 Proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6103223"}},"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":"Q4647839$5022E7E1-9532-48A5-B536-3B930DAEC381","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1eb6793bed56d8d7528b108f5ac775f3c8e59a3d","datavalue":{"value":{"text":"TLA\u2009+\u2009 Proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647839$B01B43FE-3E1C-44B9-A4CD-F6782D8AA147","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1b3c7c1306e0ca4e8e5b004874db65de3cb7d3e0","datavalue":{"value":"1372.68168","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647839$4A462A14-3135-4A0F-BC90-27932B5BF597","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ac6fe9e24507d6a0a4b79ebbf12af78cc4d41118","datavalue":{"value":"10.1007/978-3-642-32759-9_14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647839$752E78F0-F096-444C-A1C5-FAD5300DB45E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0bae40e2d630d71ea8b9d388f9791557a54f23de","datavalue":{"value":{"entity-type":"item","numeric-id":701128,"id":"Q701128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647839$DBDBD104-31DA-44E7-9DFD-3CC38F14BCAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cbf45ee236cadc75999be805a393271d5b567f30","datavalue":{"value":{"entity-type":"item","numeric-id":1868512,"id":"Q1868512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647839$65DF1862-EF18-46C5-B083-6FDF67248C8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"209ba2abb9262ee2627b025b7dc9cc61471e318c","datavalue":{"value":{"entity-type":"item","numeric-id":661001,"id":"Q661001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647839$79CF6330-A0EA-417C-87B0-2C6EFB92E365","rank":"normal"},{"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":"Q4647839$CFA75B31-0E48-4AE0-AEBA-98E998C29102","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"be7c754bd561b2fddc5eb5e378d91a8730d03353","datavalue":{"value":{"entity-type":"item","numeric-id":4647838,"id":"Q4647838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647839$C571CDD2-9062-4047-955A-CA8B340AC6C2","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":"Q4647839$A56EF8B9-AC0C-430B-A11A-3DE36D1B5142","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"47b8cd0ec3e8f1eb6cea8b605a2e9da8ee4c97b7","datavalue":{"value":{"entity-type":"item","numeric-id":4647826,"id":"Q4647826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647839$BE9CE105-441B-43B1-BA0F-D5D7F57E5393","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1fd40b453552197bf6992e0512f747c68abfc621","datavalue":{"value":{"time":"+2012-11-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4647839$011B7467-446B-4FB4-98D3-AF318043ECCC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8ac1255c5dd82b9578749cc59ec551541c683979","datavalue":{"value":"https://arxiv.org/abs/1208.5933","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647839$AC9B88F5-1896-4253-930C-DBFEEEBA2D0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P205","hash":"295f272f3475ef4178164a530a557bf922e9b9c2","datavalue":{"value":"https://hal.inria.fr/hal-00726631/file/final.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647839$86719429-2511-46BF-B08A-AC7FA84085F7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647839$2A1C0119-F406-4FEB-86B9-E21DCF114D21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647839$E93DB268-39A6-4B48-8E57-A99B2D05CC94","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8839634de897b297adfd3959ae79db169a42b46e","datavalue":{"value":"6103223","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647839$DD41B315-503E-4A32-B371-6B51A7F16622","rank":"normal"}],"P1463":[{"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":"Q4647839$AFD9BD1F-99E2-4009-83CB-02D4A5655780","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":"Q4647839$D3B14DB4-08A2-42CC-BA45-2353D2956A46","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0c7840e7c62eb9d3c28002e632f05ea0b36c8ed5","datavalue":{"value":"W4210597939","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647839$4CCBC126-52AF-4F1C-BD0F-83EE1175AE5E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7660b7808bf7a2ff2719b462cac552d7cfc45351","datavalue":{"value":{"entity-type":"item","numeric-id":4680191,"id":"Q4680191"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"83e43d94fae285e4cf3fc3e8d70f619c3f4ac922","datavalue":{"value":{"amount":"+0.8950597","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647839$08B98263-3491-4FE5-96CD-4762A451B7A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"86850ded6f45d5b101dc64f62f56e07fc50ca10b","datavalue":{"value":{"entity-type":"item","numeric-id":1914165,"id":"Q1914165"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8d61a417c60f758f859115dbad570a1080cd8fa6","datavalue":{"value":{"amount":"+0.85924727","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647839$769E27C8-B4B0-4CB4-B7B0-396AA04FD74E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"97e8e2e300ef832695287426373f19e9524a90b4","datavalue":{"value":{"entity-type":"item","numeric-id":4212930,"id":"Q4212930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0faaaf2d26549f3d05cf5d362a5a695faa213b8","datavalue":{"value":{"amount":"+0.8415996","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647839$8260D9CE-B29A-4C18-A120-4138C8C80B65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0095afed58481811d4d109a0e5ea2aaa156abc15","datavalue":{"value":{"entity-type":"item","numeric-id":3613770,"id":"Q3613770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"36aa8551df9b1d27b0f78c5ea66964d034a0f3cf","datavalue":{"value":{"amount":"+0.8402245","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647839$DF6D09F1-400E-4F1E-BC51-6700AC52EFBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"02d3f9fd26cb428cc2b03315b7b9fccf27ecfbd7","datavalue":{"value":{"entity-type":"item","numeric-id":3444802,"id":"Q3444802"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"36aa8551df9b1d27b0f78c5ea66964d034a0f3cf","datavalue":{"value":{"amount":"+0.8402245","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647839$050CFE52-3521-4BF6-8AFD-38AFBDC4610B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad894f0e4fcd4cc03c848bf583b58ab56e3b8f5c","datavalue":{"value":{"entity-type":"item","numeric-id":2753786,"id":"Q2753786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9935b359300c92843eded336283236547d280c3f","datavalue":{"value":{"amount":"+0.8397617","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647839$53CBECB2-497A-4B15-A2FA-33492AB8D56C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9155b8a24b47f93bb167596dd9931b0a708353f3","datavalue":{"value":{"entity-type":"item","numeric-id":2947464,"id":"Q2947464"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"040816e28dba1be687dffa36937e9c80756c975a","datavalue":{"value":{"amount":"+0.83899814","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647839$F085BE6F-FB02-4B70-8393-3430B588139E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0931cfd3bfa7bd1cb71152d607954b1ce96cec03","datavalue":{"value":{"entity-type":"item","numeric-id":4008744,"id":"Q4008744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c94394ab8cf671f33481dfe5d1ae6526c8a9eaa5","datavalue":{"value":{"amount":"+0.83862245","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647839$6DAFD797-5D2E-4B5C-975F-3C5B7450754C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"074fc49899c2af0bbba15842ddb799ce0c6efe54","datavalue":{"value":{"entity-type":"item","numeric-id":4885875,"id":"Q4885875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4afb41d954b89813213735407272f8720021575d","datavalue":{"value":{"amount":"+0.83803916","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647839$C58F4BBE-1C32-42CD-A0DD-83B43D344124","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":"99f62e3600009076d7030f8fe94f068c3fb69e2e","datavalue":{"value":{"amount":"+0.8374387","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4647839$98ACECCC-0EA9-4798-AE38-4CEC6FE21D00","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"TLA + Proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/TLA_%2B_Proofs"}}}}}