{"entities":{"Q6572534":{"pageid":14183689,"ns":120,"title":"Item:Q6572534","lastrevid":95765204,"modified":"2026-06-05T09:43:46Z","type":"item","id":"Q6572534","labels":{"en":{"language":"en","value":"Candle: a verified implementation of HOL light"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7881116"}},"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":"Q6572534$BC57892A-6B90-474E-8936-890816987DAE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c2b439e4efb1b987e63e5f7a423b1a4b71657b5a","datavalue":{"value":{"text":"Candle: a verified implementation of HOL light","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6572534$E913766B-2834-4F1D-A699-DB5A432A0CE3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"48bf256cb2060adcce83d6ff0339ba7814ac6cab","datavalue":{"value":{"entity-type":"item","numeric-id":1799127,"id":"Q1799127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6572534$5C049A18-D605-4505-9A16-D40538480C14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c330e55e5dc72ba4e46dcf35457734e0df28701e","datavalue":{"value":{"entity-type":"item","numeric-id":286789,"id":"Q286789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6572534$F663A7CA-9E46-4ADF-9E1C-B7C4C24C39E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"62025305e3524f61b1fc8b1f7bbd2484241846ea","datavalue":{"value":{"entity-type":"item","numeric-id":287359,"id":"Q287359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6572534$A0B0A3CB-A2F3-4E80-A9AB-99DDDA853B9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"50d312af30877232f30bb9c23fdc31fcdcb768e4","datavalue":{"value":{"entity-type":"item","numeric-id":2631536,"id":"Q2631536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6572534$F2D6FC89-F23A-4B9E-951B-7536A5E18B19","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7dae1a09e0b079923de71e99f58f11ff9161f5ec","datavalue":{"value":{"time":"+2024-07-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6572534$282785A5-67FD-40E1-97C0-B652BB51C74C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572534$B24413F5-7004-420C-AE1E-DF582EAC570E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9f31b9fdbf916da03a3501ee107861ba76f76c7b","datavalue":{"value":"7881116","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572534$A9DE8530-18B8-4072-9A17-8A03CA0FA072","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3ce15981c04e5323ddbe8904b8d560270aa9d42","datavalue":{"value":"prover soundness","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572534$FE04ABC8-22C1-4469-B5D6-E6857B0E56E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572534$10D6CBF1-C64B-4577-9B98-2605C7BAC357","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572534$7A50B41F-E0DE-4A0B-9C5C-91CB72B6A27E","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":"Q6572534$2FC00F48-90B3-4545-A216-6D0AC9298DB9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"85a29be0cb02f8355f2a4d298d6522290a3f6352","datavalue":{"value":"10.4230/LIPICS.ITP.2022.3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572534$86A53C57-4BBB-4D6D-B09B-39DDEDDE1076","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Candle: a verified implementation of HOL light","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Candle:_a_verified_implementation_of_HOL_light"}}}}}