{"entities":{"Q6190081":{"pageid":13324969,"ns":120,"title":"Item:Q6190081","lastrevid":58751868,"modified":"2026-04-06T14:27:31Z","type":"item","id":"Q6190081","labels":{"en":{"language":"en","value":"A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7800195"}},"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":"Q6190081$56A545BF-B52F-448B-96F7-BCBFE1A92DDB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2d0182d3a5a498b70c01a98f25f3d90041e91451","datavalue":{"value":{"text":"A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6190081$D61C1909-027B-4CD1-A57C-F2FC1E59A05B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"da9d0bb1bba7f8d78f26f8b0456c3cbe905220ef","datavalue":{"value":{"entity-type":"item","numeric-id":438577,"id":"Q438577"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$B10C60D4-6186-4799-B536-ABAD7605EDDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8082a87febfd862be6bce4a5ebed07469f5930e0","datavalue":{"value":{"entity-type":"item","numeric-id":496041,"id":"Q496041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$B5955816-534E-4B5F-97B1-F0D5F7D26DD3","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$D687AD97-AC9B-48D4-83F8-06600C112149","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ddc536a77b5abf6ca8dc6c14f526e73c6ecff903","datavalue":{"value":{"time":"+2024-02-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":"Q6190081$CD270CA5-A82C-484E-80D1-3011EFB138F4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"788c87d941824519b399f8f137f6502af48cb488","datavalue":{"value":"https://arxiv.org/abs/2306.12535","type":"string"},"datatype":"url"},"type":"statement","id":"Q6190081$98E60C45-AEA1-477A-9A35-46DF9F3C6B80","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6190081$450E7631-1E94-4BAD-9C8E-3F9678DACBE8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4acedbe421d28d71e58ac637a8b9c923609d4f92","datavalue":{"value":"7800195","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6190081$DB73DA28-32C5-4852-A947-CBA0BDB8FAD1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"170cc31dc4289b8b8355987c5dbf0c8c83dd2195","datavalue":{"value":"quantum information","type":"string"},"datatype":"string"},"type":"statement","id":"Q6190081$797EF604-8FB4-437E-843C-5B9979C4A91D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"996ab1bba4f0317d684cae9d0b8c156ba0c91703","datavalue":{"value":"Bell inequalities","type":"string"},"datatype":"string"},"type":"statement","id":"Q6190081$F13E2D8E-B70D-42F8-9BDF-5306DA1EF44D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q6190081$CDBAE1A3-FA66-4343-8798-C48A481F2D5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q6190081$02C1F76B-23A0-4E19-B075-1CA69AB146A3","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":"Q6190081$175BE540-1C4B-4588-A8F9-008129980E6D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"004b46dc593e1536bcc371209b5d05d4cf624a40","datavalue":{"value":"W4389978614","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6190081$8C0AC2A3-8147-4395-9750-3FAE1B9C2B26","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4738798d9702e646d9743f53f948745583da971","datavalue":{"value":{"entity-type":"item","numeric-id":2352487,"id":"Q2352487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$6530EE64-867C-41A9-9265-85D42188266B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af5a7e6ac670e3a59be91a1dedb7e84424f42bd8","datavalue":{"value":{"entity-type":"item","numeric-id":5015189,"id":"Q5015189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$746D8BC4-FDC0-4514-B87E-AC752A2EA0D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad66d8c8284793fd499f5f09ca59cf54c6ecb95a","datavalue":{"value":{"entity-type":"item","numeric-id":2666954,"id":"Q2666954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$B32D6E42-D33F-48B5-9834-6F5ABF820E9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a8078cd37e261a0989a85da3d6b72e3d7a45d46","datavalue":{"value":{"entity-type":"item","numeric-id":5094472,"id":"Q5094472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$584E855B-61BC-40B2-BACA-94D524CF4BD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e041061ee949ed7edbbc5a780954999c7edae27","datavalue":{"value":{"entity-type":"item","numeric-id":964475,"id":"Q964475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$08E6C46B-8EA7-46A3-B2F8-8B55BE15A6F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ec07cadcdae1567684f00ac38988b780c4f7ed4","datavalue":{"value":{"entity-type":"item","numeric-id":964473,"id":"Q964473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$16AA1043-85E6-4274-9167-359464D6AB47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e4df1fbe284d5fc9f37495f92c778c1ff839b7d","datavalue":{"value":{"entity-type":"item","numeric-id":2233453,"id":"Q2233453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$317C7FA6-7395-4FF3-A98C-0AE4D5E0EAE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a41c48ae033d6a021f1ff3a4e0ed4f08f4c95ff3","datavalue":{"value":{"entity-type":"item","numeric-id":5363832,"id":"Q5363832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$877E3AFB-C31D-4EED-8D7A-79A3BD879AB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9d4c497fb6c1130d68266bfc3951a0b212649a6","datavalue":{"value":{"entity-type":"item","numeric-id":3999383,"id":"Q3999383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$8FE0C6D7-10A2-4C72-B213-5102AAADB51F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e352700e89e42c8d944f800e628d3e41526eb326","datavalue":{"value":{"entity-type":"item","numeric-id":5758664,"id":"Q5758664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$0E774CF4-043D-4046-8F5A-A2357F1AB926","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1430057f5b02d1dc624f03f2f455e2ceeb0c0624","datavalue":{"value":{"entity-type":"item","numeric-id":5836035,"id":"Q5836035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$03663960-6949-427F-8557-C0122A18C665","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aef451875908e4a4b8b42306f28a4c3131588609","datavalue":{"value":{"entity-type":"item","numeric-id":5871067,"id":"Q5871067"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$1DC3C474-ADC3-4CA8-A25A-DA91170FCC62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a1a0dcbfc561e1e5ffac774e9501a5c3c966797","datavalue":{"value":{"entity-type":"item","numeric-id":1722645,"id":"Q1722645"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$E3341518-0BD3-4BA4-98D7-0E3534CEF1CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f96e3cd73827723a8dc982d846104e251d12bb4f","datavalue":{"value":{"entity-type":"item","numeric-id":6154880,"id":"Q6154880"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$E83F4F6C-B30B-4811-943B-651D4D58C0AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e264974062f53b439460b85662778a60b49509d","datavalue":{"value":{"entity-type":"item","numeric-id":2926333,"id":"Q2926333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$37325B4E-C2F7-4FAA-A7E2-F85DF6E889A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e194fd5d50acb378b801bdc31f6fcb44d1092a9a","datavalue":{"value":{"entity-type":"item","numeric-id":3384929,"id":"Q3384929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$77BB5EE9-B83A-4579-A455-F93606A39B29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d50d5d113dba2ca0ebc00b774681283fd48f107","datavalue":{"value":{"entity-type":"item","numeric-id":5227999,"id":"Q5227999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$15713334-9954-41C9-A42B-793FD6A5F0A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df5f93ee6a15cce013d1f3bb4d676b560e5816a7","datavalue":{"value":{"entity-type":"item","numeric-id":5380631,"id":"Q5380631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$6A323719-A124-4185-8B3E-33A0AED5555B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c68119d731889bb894378428c10b0f40a0e388d","datavalue":{"value":{"entity-type":"item","numeric-id":2816299,"id":"Q2816299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6190081$2325B4A5-06E4-4AE9-AB63-865574DC4A5C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"495cc6037621554d5baefd9c00009bf87b083ba6","datavalue":{"value":"10.1007/S10817-023-09689-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6190081$60650020-6F6E-4621-AE6B-7D70EDA9938B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6190081","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6190081"}}}}}