{"entities":{"Q7361584":{"pageid":31520291,"ns":120,"title":"Item:Q7361584","lastrevid":105367358,"modified":"2026-10-07T13:36:56Z","type":"item","id":"Q7361584","labels":{"en":{"language":"en","value":"Algorithms for Reduced Ordered Binary Decision Diagrams"}},"descriptions":{"en":{"language":"en","value":"AFP entry ROBDD"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"aeed90c9de8f501775d9626266ca1b7dfe44de42","datavalue":{"value":"https://isa-afp.org/entries/ROBDD.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361584$6F0F86F7-D43A-4A42-B397-B1EBF1850376","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6bab1e04a2dd935c04e3f5ad0d3bd237dec213f4","datavalue":{"value":{"time":"+2016-04-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361584$B55E09EE-1A46-4F7A-91F7-E94F56BE3E3E","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"045dde749400578820aeaa85be8498af97b18250","datavalue":{"value":"Julius Michaelis","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361584$F8CF37C0-3355-4251-9168-63B6069C5BA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"3e24c85cc74f22f9901f70520869c19fde2b00ac","datavalue":{"value":"Max W. Haslbeck","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361584$EC8E38EE-E1EB-43C0-BA8B-5976DC3FD9D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"7545c5768cca6bd4b47e52bfec18c22cb81849df","datavalue":{"value":"Peter Lammich","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361584$36B78832-2FDF-40EB-806A-C48AC7EEB288","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"bf5d485796582ea615cfd5e7c0148e1add1641d3","datavalue":{"value":"Lars Hupel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361584$4581AD40-B17F-407A-B173-44D84D5E5BD6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ac9f8d4ff6e8002ba5eca846d01be8d3a83f2e38","datavalue":{"value":{"text":"Algorithms for Reduced Ordered Binary Decision Diagrams","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361584$4C2CDC54-4710-47AA-B5AA-AFECC9C9A6AD","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"c1f079b7ac777b6d8ba1439abbc3908168714f97","datavalue":{"value":"We present a verified and executable implementation of ROBDDs in Isabelle/HOL. Our implementation relates pointer-based computation in the Heap monad to operations on an abstract definition of boolean functions. Internally, we implemented the if-then-else combinator in a recursive fashion, following the Shannon decomposition of the argument functions. The implementation mixes and adapts known techniques and is built with efficiency in mind.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361584$C75F2CDD-4E45-42E6-B428-6FAF528A90A9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e960d98de80954b9ec32fb5001729a0d785cd21e","datavalue":{"value":{"entity-type":"item","numeric-id":4647844,"id":"Q4647844"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361584$390BFBB9-916C-48AC-90F9-51A200573D63","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":"Q7361584$E682F62D-8338-4284-984E-5F321DB1AD65","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"27e971e25f48a406ca09caf18a9e463d40cb63ef","datavalue":{"value":{"entity-type":"item","numeric-id":7361166,"id":"Q7361166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361584$F16A1B78-D4A7-4E09-B392-C5A1E61E6D42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"f0d6ccc9a00d2d1e3be7ec2239689671c14dec25","datavalue":{"value":{"entity-type":"item","numeric-id":7361918,"id":"Q7361918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361584$6FB72646-2554-44C0-BE9C-F43F587FE351","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"1518b44e9920a7e58377edf0d25bb1683f308560","datavalue":{"value":{"entity-type":"item","numeric-id":7361163,"id":"Q7361163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361584$FB7439D3-178B-49DE-A21E-DBE0042EECF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"6df1e1600a3acc40d1b0a9c9cf7cbc177462ddf9","datavalue":{"value":{"entity-type":"item","numeric-id":7361373,"id":"Q7361373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361584$4EB15F2F-6506-402F-9C35-E9FF6D07E5F3","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"1157f6239d5752bb0ad1cee836272bd46c6bf40f","datavalue":{"value":{"entity-type":"item","numeric-id":7360772,"id":"Q7360772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361584$0BB0391B-D6DD-437F-AA68-299B78085FE5","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":"Q7361584$9E4D40BE-AC5E-45C9-A525-9E7E8E9D59A3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Algorithms for Reduced Ordered Binary Decision Diagrams","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Algorithms_for_Reduced_Ordered_Binary_Decision_Diagrams"}}}}}