论文标题
依赖性键入知识图
Dependently Typed Knowledge Graphs
论文作者
论文摘要
知识图上的推理传统上是基于语义网络堆栈中语言的层次结构构建的。从资源描述框架（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.
