依赖类型的知识图谱
Dependently Typed Knowledge Graphs
摘要：
在知识图谱上的推理传统上是建立在语义Web堆栈中的语言层次结构上的。从用于知识图谱的资源描述框架（RDF）开始，通过各种语法扩展引入了更高级的构造，以向知识图谱添加推理功能。在本文中，我们将展示如何标准化的语义Web技术（RDF及其查询语言SPARQL）可以再现在一个统一的方式与依赖类型论。除了提供知识图谱的基本功能之外，依赖类型还增加了实体和查询编码的表达性、通过证人对查询的回答的可解释性以及证人构建的组合性和自动化。使用Coq证明助手，我们演示了如何建立和查询依赖类型的知识图谱，作为未来在这个方向上的工作的概念证明。
英文摘要：
Reasoning over knowledge graphs is traditionally built upon a hierarchy of languages in the Semantic Web Stack. Starting from the Resource Description Framework (RDF) for knowledge graphs, more advanced constructs have been introduced through various syntax extensions to add reasoning capabilities to knowledge graphs. In this paper, we show how standardized semantic web technologies (RDF and its query language SPARQL) can be reproduced in a unified manner with dependent type theory. In addition to providing the basic functionalities of knowledge graphs, dependent types add expressiveness in encoding both entities and queries, explainability in answers to queries through witnesses, and compositionality and automation in the construction of witnesses. Using the Coq proof assistant, we demonstrate how to build and query dependently typed knowledge graphs as a proof of concept for future works in this direction.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
