{"entities":{"Q40546":{"pageid":40602,"ns":120,"title":"Item:Q40546","lastrevid":105427025,"modified":"2026-10-09T10:06:40Z","type":"item","id":"Q40546","labels":{"en":{"language":"en","value":"Constructive Proof FLP"}},"descriptions":{"en":{"language":"en","value":"AFP entry FLP"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"201e81638008b7e867a716570bd361b79cd3b403","datavalue":{"value":"28832","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40546$CDE8650F-E93D-46EF-ADB8-7160175CE970","rank":"normal"}],"P286":[{"mainsnak":{"snaktype":"value","property":"P286","hash":"6b7c4989a2f0355d4de64322de5416789745a8f0","datavalue":{"value":{"entity-type":"item","numeric-id":2829253,"id":"Q2829253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$497A5DC8-9A5D-4796-9366-A732D487D034","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$A2539715-EE4C-481B-AA2D-B414F9B699E7","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"a5c6cca351ef8eb8729a2208c381f5030271336a","datavalue":{"value":"https://www.isa-afp.org/entries/FLP.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40546$E73BEB4B-6487-4765-A5D6-25B6443A8F19","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40546$A5E2ACED-7FB8-4295-8B78-36F453AF2748","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$944C011D-6B66-45FE-9291-FA1D1794C2E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a0e5265d89b950e95ee0840ba1ad9160d4d6d538","datavalue":{"value":{"entity-type":"item","numeric-id":34458,"id":"Q34458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$2522E4C4-02F6-47A5-9967-8215D11FC144","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ce3647fc4493c07827244cf82891c972b7202e92","datavalue":{"value":{"entity-type":"item","numeric-id":33502,"id":"Q33502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$823DAF52-9D2C-4794-8756-A496483FFDD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc4eff68b160f30b8d66dfcb610a0ea7a927079b","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$02782AE6-A588-4024-9ACD-E6487C56E2FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"346bb06feebe5eec8261e483309d0da7485c1091","datavalue":{"value":{"entity-type":"item","numeric-id":21467,"id":"Q21467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$41B9A7C7-809F-4B87-B108-9F3CE55EE83A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a1682e4f3c5b07f98f0ac9d21e07e98858926fb0","datavalue":{"value":{"entity-type":"item","numeric-id":5972585,"id":"Q5972585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$FB6FFFBF-F418-4AFE-85B2-28BD11F6F33E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ed15eb8701a335444fde1bcc3327d1067ce64751","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$B5981412-ABFB-4945-8B87-0B465EF663DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9e7a1624ebcfc86cb11ccad80d0985ed6ed992b9","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$30AF8B8E-2071-487C-B43F-131351BBEF83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$F1A54A95-26CB-4F8B-82E8-54267A17F87D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$A2510E5F-8107-4302-85FD-219F58ACCDE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$473E6607-44E9-45EC-8FF1-A969C96908A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$8DB5BB9D-D690-493D-92BF-CBAB98032399","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"79e0d2557f2d00c54ab1d6c9bc495e2798294902","datavalue":{"value":"https://isa-afp.org/entries/FLP.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40546$6DA8D7E7-6D15-4E16-AC40-ECEA94D9E948","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"f9ca340aa87216db3545ff3ff7b803c99d91513c","datavalue":{"value":"Benjamin Bisping","type":"string"},"datatype":"string"},"type":"statement","id":"Q40546$72056E90-D1A3-42D5-9F89-5B7C12C989F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"896e708b8fb664672390afac9965f6bab65e65b6","datavalue":{"value":"Paul-David Brodmann","type":"string"},"datatype":"string"},"type":"statement","id":"Q40546$1F8E608B-1FDB-4AA1-BC3F-04D71A5BF758","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"1ec86844d4e913fbc68d47d8cd8e1a4b31541a62","datavalue":{"value":"Tim Jungnickel","type":"string"},"datatype":"string"},"type":"statement","id":"Q40546$397E0C96-7B86-42D2-87EF-733C9E9466B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"c3cf90a4f6a15bbec4798b2e0cb4fcf87ed73c27","datavalue":{"value":"Christina Rickmann","type":"string"},"datatype":"string"},"type":"statement","id":"Q40546$1012F567-89E2-4375-B723-FC926377CE0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"0537792aa728632bed9592eded4ff59ea9d19684","datavalue":{"value":"Henning Seidler","type":"string"},"datatype":"string"},"type":"statement","id":"Q40546$6C1C1578-1695-4B56-8B77-C2F826AF8917","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"0c42f8fbbfe4543ff9c3e3bf08a696ba12e9a0f1","datavalue":{"value":"Anke St\u00fcber","type":"string"},"datatype":"string"},"type":"statement","id":"Q40546$956D2859-9E5B-4539-88C7-FC9484C84E52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"0747fc165d2b9ac0fe3abaef14d2606c936d4fa5","datavalue":{"value":"Arno Wilhelm-Weidner","type":"string"},"datatype":"string"},"type":"statement","id":"Q40546$2B8ADE2F-E985-4644-805A-7485B9253F11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"6f078f2476577e7cf269b66494f23c23a31850d3","datavalue":{"value":"Kirstin Peters","type":"string"},"datatype":"string"},"type":"statement","id":"Q40546$D165C116-D8D0-4DBA-92EE-05D255E95A18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"ebafe67ea91088873a9fa9c8068ace3e7d8b7190","datavalue":{"value":"Uwe Nestmann","type":"string"},"datatype":"string"},"type":"statement","id":"Q40546$F8973FF3-CAC1-4BAF-899B-A61EF67F8E00","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f87118978f5e5b6a89a40cf2adb3f4b8d3460cd6","datavalue":{"value":"The impossibility of distributed consensus with one faulty process is a result with important consequences for real world distributed systems e.g., commits in replicated databases. Since proofs are not immune to faults and even plausible proofs with a profound formalism can conclude wrong results, we validate the fundamental result named FLP after Fischer, Lynch and Paterson. We present a formalization of distributed systems and the aforementioned consensus problem. Our proof is based on Hagen V\u00f6lzer's paper \"A constructive proof for FLP\". In addition to the enhanced confidence in the validity of V\u00f6lzer's proof, we contribute the missing gaps to show the correctness in Isabelle/HOL. We clarify the proof details and even prove fairness of the infinite execution that contradicts consensus. Our Isabelle formalization can also be reused for further proofs of properties of distributed systems.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40546$9B69EC6E-925A-46BC-B1C0-CE4AE94D6D2D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"61b2be8630819c0185168a7a93ceacaa68493468","datavalue":{"value":{"entity-type":"item","numeric-id":3664419,"id":"Q3664419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$8EC38845-90EA-4F95-B580-864197AADB21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$9086E62A-7E8B-437F-8BD9-C646DF87E0FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26f9c9c0da0bc3bdb62c24d5a0777f8a36a55f99","datavalue":{"value":{"entity-type":"item","numeric-id":3766835,"id":"Q3766835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$E1547500-50B2-44DB-B017-1D0928719141","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34e771030942e4f129dddceb8d1ab2bb76680f85","datavalue":{"value":{"entity-type":"item","numeric-id":1392214,"id":"Q1392214"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$3850B63F-BF27-4E03-9619-4642FCBAB941","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1106cea0d8c864d01c8334e7dbc957d137ef7695","datavalue":{"value":{"entity-type":"item","numeric-id":834901,"id":"Q834901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$9603C9B7-D97D-48F4-B955-E6DA41C5FFD7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"520e6f0241f1a69086f50367d5722006ec0b624b","datavalue":{"value":{"time":"+2016-05-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40546$690FF949-C41F-4CA0-88D4-DF29F5B87603","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d2acee70d86d6daf045409781628a4b5a4a9356b","datavalue":{"value":{"text":"A Constructive Proof for FLP","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40546$A293B35D-1602-4309-AEAA-64EA44EE2BD5","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$B0105F16-708F-468D-BD0F-485B4CDF23B3","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"d4e45a44d8cb21e0bc3c4e18fb1edc38a1545452","datavalue":{"value":{"entity-type":"item","numeric-id":7360785,"id":"Q7360785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40546$3F4BA1BA-26CB-4EBE-BFE3-45E5F58EF435","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Constructive Proof FLP","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Constructive_Proof_FLP"}}}}}