{"entities":{"Q7361427":{"pageid":31519820,"ns":120,"title":"Item:Q7361427","lastrevid":105365900,"modified":"2026-10-07T13:36:19Z","type":"item","id":"Q7361427","labels":{"en":{"language":"en","value":"Positional Determinacy of Parity Games"}},"descriptions":{"en":{"language":"en","value":"AFP entry Parity_Game"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e4b15702fc65cf744f1db237a9170f3c4ce224db","datavalue":{"value":"https://isa-afp.org/entries/Parity_Game.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361427$2A3FFF29-D487-4F0E-AF1B-32DB280D066A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"49c905baf0f1483cbda0527efa721826b9ca8c8f","datavalue":{"value":{"time":"+2015-11-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361427$D5C1EF23-A215-4CAA-B2E1-CF1CC75DE969","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"f49b1351385a885d620f54347daa078a5855fc73","datavalue":{"value":"Christoph Dittmann","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361427$7F7F3C66-44F8-4716-9231-1E77E6695364","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"aff0cc90a075f38be3841d26366635e27efc45d0","datavalue":{"value":{"text":"Positional Determinacy of Parity Games","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361427$9B8B27AB-CA32-49AD-8543-298DEB85BF00","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"5dd12fd647b3deb6ae3edcd15a3a9f92bb6e8b2e","datavalue":{"value":"We present a formalization of parity games (a two-player game on directed graphs) and a proof of their positional determinacy in Isabelle/HOL. This proof works for both finite and infinite games.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361427$1441E0B4-93FA-4588-BFF4-CDCD45059D47","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"90baa942460aa8b4cf3c97f6d2c7362fb5539324","datavalue":{"value":{"entity-type":"item","numeric-id":4412829,"id":"Q4412829"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361427$C9E523D6-1BCC-4A96-8C52-9055D65813A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ee0f06f8149ad9449d52f3e00709cc707f14bc42","datavalue":{"value":{"entity-type":"item","numeric-id":1276252,"id":"Q1276252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361427$5BDF71BF-E07A-4A2A-B18F-1C332ABCA7F2","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":"Q7361427$DD31822C-2337-4CA4-8FD7-1CFBFD8FC656","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"c9d73c02403c0af647a73b8da7299dbef78ebf0b","datavalue":{"value":{"entity-type":"item","numeric-id":7361764,"id":"Q7361764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361427$0A485C26-D872-49BE-90ED-8F2A6726F892","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"b999678a517221bed9bd614caca8006ebca3a529","datavalue":{"value":{"entity-type":"item","numeric-id":7361796,"id":"Q7361796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361427$218DF1C5-04BD-467F-846E-B0A10A9E19F2","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"a72569ac3fa7d166ec3d63a25d7f4970dd09f6f6","datavalue":{"value":{"entity-type":"item","numeric-id":7360825,"id":"Q7360825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361427$4A838AF5-0EBC-4462-974D-F0E1073C2758","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":"Q7361427$9A90339C-D803-4819-919A-AF8E5515867E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Positional Determinacy of Parity Games","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Positional_Determinacy_of_Parity_Games"}}}}}