{"entities":{"Q7361932":{"pageid":31521335,"ns":120,"title":"Item:Q7361932","lastrevid":105370505,"modified":"2026-10-07T13:39:10Z","type":"item","id":"Q7361932","labels":{"en":{"language":"en","value":"B\u00fcchi Complementation"}},"descriptions":{"en":{"language":"en","value":"AFP entry Buchi_Complementation"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6475c212fccacc20836e20f9af7e03d1133c456c","datavalue":{"value":"https://isa-afp.org/entries/Buchi_Complementation.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361932$87CBB1CA-7291-4978-8344-181FF0A7E5C5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"09fed704422914cfe2a4482b61f3f610c89a1884","datavalue":{"value":{"time":"+2017-10-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361932$BD283D99-51D3-4721-AF8A-ABC9A8D8C564","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"858e1b98f2a2702d86b0690e1e15aa540fc68e16","datavalue":{"value":"Julian Brunner","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361932$25C4C84E-9EC0-47DC-BDF5-F40A7F073E5A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"eaf27dec02842b7e1c6879a76f6e5bfc2d54aa64","datavalue":{"value":{"text":"B\u00fcchi Complementation","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361932$6087F6D2-6208-4B94-B03E-05E230230297","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"2e0a51f4ae8404d1b6b6068f902e78c3eeecc887","datavalue":{"value":"This entry provides a verified implementation of rank-based B\u00fcchi Complementation. The verification is done in three steps: Definition of odd rankings and proof that an automaton rejects a word iff there exists an odd ranking for it. Definition of the complement automaton and proof that it accepts exactly those words for which there is an odd ranking. Verified implementation of the complement automaton using the Isabelle Collections Framework.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361932$CAC30F2F-459E-4970-8A05-537BB51A9DB2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"fdbace6415d89fca5d9ba31adb1a3b4e1ba6373e","datavalue":{"value":{"entity-type":"item","numeric-id":3549125,"id":"Q3549125"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361932$E6516068-1633-49C8-810F-A995B9173335","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":"Q7361932$F10C1CA5-DCC9-40CA-A660-734B3F6D9FD8","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"4571af89e2882a45bee5f9e442723910fbf0c144","datavalue":{"value":{"entity-type":"item","numeric-id":7361382,"id":"Q7361382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361932$3A0A99A5-2837-4585-B1E5-C96A794E13D6","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"73d93a21b0749f7f2c51d7daeb11b162660cd756","datavalue":{"value":{"entity-type":"item","numeric-id":7360784,"id":"Q7360784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361932$B98624D0-B2B2-4A5F-853B-D5A56DFBE18A","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":"Q7361932$D8402241-388E-4E18-93E9-AE986494522A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"B\u00fcchi Complementation","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/B%C3%BCchi_Complementation"}}}}}