Dependently Typed Knowledge Graphs
This work addresses the need for more expressive and explainable reasoning in knowledge graphs for semantic web applications, though it is incremental as it builds on existing technologies with a new theoretical framework.
The paper tackled the problem of reasoning over knowledge graphs by reproducing standardized semantic web technologies (RDF and SPARQL) using dependent type theory, resulting in a unified approach that adds expressiveness, explainability, and automation to knowledge graph queries through a proof-of-concept implementation in 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.