{"entities":{"Q6862767":{"pageid":20673223,"ns":120,"title":"Item:Q6862767","lastrevid":75173389,"modified":"2026-04-18T02:31:54Z","type":"item","id":"Q6862767","labels":{"en":{"language":"en","value":"Candle: a verified implementation of HOL Light (extended version)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8155890"}},"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":"Q6862767$0E96A7E0-7073-4AD9-9B53-CBEA7CD501DD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"66e6238353f720dd7a4a8fd5a5a4e429308846bf","datavalue":{"value":{"text":"Candle: a verified implementation of HOL Light (extended version)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6862767$E62054E7-BF63-4818-9848-ECBED7A44806","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6194027a763b313428fce4e79ce5153422a2265a","datavalue":{"value":"10.1007/S10817-025-09743-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6862767$1BF294B0-1D32-49FD-B3C3-9087E43C1427","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":"Q6862767$547CA0D8-D0AC-402D-9DAE-3A2A2008F24A","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":"Q6862767$4A2AB6B0-8547-4623-BDE7-8BD21DC6A4C3","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":"Q6862767$B0C9C6AE-0643-47E3-8443-B0EBF8074D5E","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":"Q6862767$2E2D3DEE-6554-42E4-9853-9672BD491A6E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$A5571280-9BE2-400B-B3B8-0806C01D6CAA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"fc57803b76bc19bf04798b0b41d601913e68dca7","datavalue":{"value":{"time":"+2026-02-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6862767$05D6A6B0-9333-43F1-9110-04BC0341A953","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6862767$035670D0-7BCF-4D76-B78E-64A7310D865F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a236ba26796f05e945f9718a6f628c2ab45b00ba","datavalue":{"value":"8155890","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6862767$0A866381-B8DD-425A-9627-8123C6F8674D","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$7B83F146-4A3B-4693-8330-ADCE700C67E2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3ce15981c04e5323ddbe8904b8d560270aa9d42","datavalue":{"value":"prover soundness","type":"string"},"datatype":"string"},"type":"statement","id":"Q6862767$BB6B4A34-5C1E-4FDE-A620-5F00CF7EB6B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6862767$2DF713EF-89E8-45E0-8F1C-3495BBDE4C5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6862767$AFC7B03E-0E60-41B8-A45C-B0D4775535E4","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":"Q6862767$9C6904BA-36B2-4D8D-BEAB-B6ABA6387545","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Candle: a verified implementation of HOL Light (extended version)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Candle:_a_verified_implementation_of_HOL_Light_(extended_version)"}}}}}