Dependently Typed Knowledge Graphs
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Knowledge GraphsSimilar Papers 제목 키워드 기반
Enhanced Knowledge Graphs Using Typed Entailment Graphs
Constructing knowledge graphs from open-domain corpora is a crucial stage in question answering. Most previous works are based on open information extraction methods, which extract relations by parsing sentences into t…
Knowledge GraphsOpen Information ExtractionQuestion AnsweringTheorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint
Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type the…
Automated Theorem ProvingTranslationMissDiag: Diagnostic Evaluation of Incomplete-Knowledge Robustness in KGQA and KG-RAG
Knowledge graph question answering (KGQA) and knowledge-graph-based retrieval-augmented generation (KG-RAG) aim to ground answers in explicit graph evidence, but real-world knowledge graphs are often sparse, outdated, an…
Graph Question AnsweringKnowledge GraphsDependently-Typed Montague Semantics in the Proof Assistant Agda-flat
Grokers: Bottom-Up Inductive Comprehension and Write-Time Intelligence over Typed Knowledge Graphs
We present Grokers, an architecture for building persistent, structured comprehension of typed knowledge graphs through bottom-up inductive traversal of dependency subgraphs. Unlike retrieval-augmented generation (RAG), …
Knowledge Graphs