Over the past two decades, the Web Ontology Language (OWL) has been instrumental in advancing the development of ontologies and knowledge graphs, providing a structured framework that enhances the semantic integration of data. However, the reliability of deductive reasoning within these systems remains challenging, as evidenced by inconsistencies among popular reasoners in recent competitions. This evidence underscores the limitations of current testing-based methodologies, particularly in high-stakes domains such as healthcare. To mitigate these issues, in this paper, we have developed VEL, a formally verified EL++ reasoner equipped with machine-checkable correctness proofs that ensure the validity of outputs across all possible inputs. This formalization, based on the algorithm of Baader et al., has been transformed into executable OCaml code using the Coq proof assistant's extraction capabilities. Our formalization revealed several errors in the original completeness proofs, which led to changes to the algorithm to ensure its completeness. Our work demonstrates the necessity of mechanization of reasoning algorithms to ensure their correctness at theoretical and implementation levels.

翻译：过去二十年间，Web本体语言（OWL）在推动本体与知识图谱发展方面发挥了关键作用，其提供的结构化框架显著增强了数据的语义集成能力。然而，这些系统中的演绎推理可靠性仍面临挑战，近期竞赛中主流推理器之间的结果不一致现象便是有力佐证。这一现象凸显了当前基于测试的方法论存在局限性，在医疗健康等高风险领域尤为突出。为缓解这些问题，本文开发了VEL——一个配备机器可检验正确性证明的形式化验证EL++推理器，该证明能确保所有可能输入条件下输出结果的有效性。此项基于Baader等人算法的形式化工作，通过Coq证明助手的代码提取功能被转化为可执行的OCaml代码。我们的形式化过程揭示了原始完备性证明中的若干错误，进而促使对算法进行修正以确保其完备性。本研究表明，对推理算法进行机械化验证对于保障其理论与实现层面的正确性具有必要性。