VEL：一个形式化验证的 OWL2 EL 配置文件推理器
计算机科学中的逻辑
2024-12-13 v1 人工智能
编程语言
摘要
过去二十年来，维基百科语言（OWL）在推动本体法和知识图谱的发展方面发挥了重要作用，提供了结构化框架，增强了数据的语义集成。然而，这些系统中演绎推理的可靠性仍然具有挑战性，正如近期比赛中各大推理器之间不一致性所证明的那样。这一证据凸显了当前基于测试的方法的局限性，尤其是在诸如医疗保健等高风险领域。为缓解这些问题，本文中我们开发了 VEL，一个经过形式化验证的 EL++ 推理器，配备机器可检查的正确性证明，确保其在所有可能输入上的输出有效性。该形式化基于 Baader 等人的算法，通过 Coq 证明助手的提取功能将其转化为可执行的 OCaml 代码。我们的形式化揭示了原始完整性证明中的多个错误，导致对算法进行更改以确保其完整性。我们的工作表明，对推理算法进行机械化处理是确保其在理论和实现层面正确性所必需的。
引用
@article{arxiv.2412.08739,
title = {VEL: A Formally Verified Reasoner for OWL2 EL Profile},
author = {Atalay Mert Ileri and Nalen Rangarajan and Jack Cannell and Hande McGinty},
journal= {arXiv preprint arXiv:2412.08739},
year = {2024}
}