{"entities":{"Q6862767":{"pageid":20673223,"ns":120,"title":"Item:Q6862767","lastrevid":84246878,"modified":"2026-05-14T04:04:05Z","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"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9990a2e16f4d96fb2dc6e7fcff54427a1d73f706","datavalue":{"value":{"entity-type":"item","numeric-id":3088011,"id":"Q3088011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$82040877-4BD7-46AA-BA8A-D976DD19878E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f4334b25d43b9293350a877e2d317280ca55a9","datavalue":{"value":{"entity-type":"item","numeric-id":3543646,"id":"Q3543646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$984AECB5-B272-4AE8-8BEC-18DE7949C544","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c704d43a48e07ac24cfe13985bec3bdd1a17595","datavalue":{"value":{"entity-type":"item","numeric-id":834373,"id":"Q834373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$F10CB33D-07F8-4B17-A4CC-2E2DB55B2218","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4d5de220317fd709a7e63acdecfb92f5c42b492","datavalue":{"value":{"entity-type":"item","numeric-id":2280211,"id":"Q2280211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$5E5EADE0-3240-49F7-875E-8443FDBD9F9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"457ec7d32f0f86f3bbf301599db4ae5da346089d","datavalue":{"value":{"entity-type":"item","numeric-id":6572534,"id":"Q6572534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$0F7969C4-3535-4B65-BBB8-356D8D07A3C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b125e9042a33a4fe7a2c681741f4499aa86fd0d","datavalue":{"value":{"entity-type":"item","numeric-id":7009612,"id":"Q7009612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$1803AD71-3FEC-4F93-A8E4-5AF1961E1D51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"92281f917da3a00fe0192413035ae6a90371a0b1","datavalue":{"value":{"entity-type":"item","numeric-id":287361,"id":"Q287361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$C16F56CD-1697-42E9-8B84-BD847544E27E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d93e889c52c36a6fb58e10f9eb9b5078b5353ce","datavalue":{"value":{"entity-type":"item","numeric-id":4972072,"id":"Q4972072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$E9CA1927-02A1-4B5F-A23E-26A09EA49B14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"227fe77aa9bac83e88e8a7622effb8e94001c51a","datavalue":{"value":{"entity-type":"item","numeric-id":2875232,"id":"Q2875232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$7F933846-09FE-4A2F-AC4C-3F15EEC266F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"967f62bb611922786597b809e2544b21014e772a","datavalue":{"value":{"entity-type":"item","numeric-id":2208292,"id":"Q2208292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$4B96D4DC-EF97-4965-908F-EEEE888BF61C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d570704f2bdc1a845c42ed053316a109277d5c82","datavalue":{"value":{"entity-type":"item","numeric-id":2829240,"id":"Q2829240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$4E15B4E6-18B2-430A-94F1-06DAFFC450AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aeedc506ee95714a79cfc16f82862182df8774bc","datavalue":{"value":{"entity-type":"item","numeric-id":3613408,"id":"Q3613408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$22B6313A-FF50-4B7F-B72F-69BE14C7D230","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b6df3cfdd6a5466641b3d099b42234a2ae22d485","datavalue":{"value":{"entity-type":"item","numeric-id":7024188,"id":"Q7024188"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$9063F74E-824A-4B05-88F2-4103D762815E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f63882d8148fc3fd80571ef07ea5324b0da4d29","datavalue":{"value":{"entity-type":"item","numeric-id":6940472,"id":"Q6940472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$416578A2-9CC0-4B90-B706-941057BBBEC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"308c41ebef7842c97dab1c1ac8712465db75f49b","datavalue":{"value":{"entity-type":"item","numeric-id":6572550,"id":"Q6572550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$A94F69C9-02CD-42EA-AB20-415AA742CF64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc9d0044875a173a7ecf2471ca493b7ca43f1fb7","datavalue":{"value":{"entity-type":"item","numeric-id":2055847,"id":"Q2055847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$3908424D-E20E-4D76-9A13-B0165E66866A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fcd44752aa5df5cd038054d2d30c6001d6392b03","datavalue":{"value":{"entity-type":"item","numeric-id":286790,"id":"Q286790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$9C493C6C-09AF-47B1-AAD8-32D6A13ED836","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1689dae40df2cd1bdc239cd12cf0ee26dcff3698","datavalue":{"value":{"entity-type":"item","numeric-id":2219381,"id":"Q2219381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$589CFF8F-B72C-43ED-AA33-4824789B6F7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"739330a58a3c3aae77075c5fb847ca13d50160d0","datavalue":{"value":{"entity-type":"item","numeric-id":3075242,"id":"Q3075242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$0EB30F47-6F08-49D0-A7BF-E31CB64FA51B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9864722e1120856743b1e5eb3761fb8bcb430e4","datavalue":{"value":{"entity-type":"item","numeric-id":2879241,"id":"Q2879241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6862767$3436D05A-8C71-45EB-8A77-7768E3C5438B","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)"}}}}}