Bringing Mathematical Rigor to Knowledge Graphs: The Promise of Dependent Type Theory

In the age of artificial intelligence and big data, knowledge graphs have become foundational infrastructure for organizing and querying information. From powering Google’s search results to managing private company data, these graph-based databases store relationships between entities in a way that machines can understand and reason about. But what if there was a way to make knowledge graphs not just more accurate, but also more explainable and verifiable?

A recent research paper by Lai, Ng, Wong, See, and Lin from NVIDIA AI Technology Centre, Singapore University of Technology and Design, and the Institute of High Performance Computing introduces an innovative approach: Dependently Typed Knowledge Graphs (DTKGs). Their work demonstrates how techniques from mathematical logic and formal verification can address critical challenges in knowledge graph reasoning, particularly the thorny problem of provenance — tracking how we know what we know.

The Problem with Traditional Knowledge Graphs

Current knowledge graph technologies, built on the Semantic Web Stack, use the Resource Description Framework (RDF) to represent information as triples: a subject, a predicate, and an object. For example, “Barack is the father of Sasha” would be represented as the triple (Sasha, hasFather, Barack).

However, this approach has limitations:

1. Weak type enforcement: While RDF Schema (RDFS) allows you to specify that a “father” relationship should connect two “Person” entities, these specifications aren’t enforced. You could accidentally create a relationship like “Chicago is the father of Barack” without triggering any errors.
2. Lack of provenance: If a knowledge graph contains the claim that “Barack is the father of Malia,” it’s unclear whether this is directly evidenced by a birth certificate or inferred from other relationships like “Barack is the husband of Michelle” and “Michelle is the mother of Malia.”
3. Limited explainability: When machines derive new information from existing knowledge, there’s no built-in mechanism to explain how that derivation occurred.

Enter Dependent Type Theory

The researchers propose using dependent type theory — a powerful framework from mathematical logic that underlies proof assistants like Coq, Agda, and Lean — as the foundation for knowledge graphs.

In this approach, every entity and relationship is assigned a precise type, and these types can depend on values. This is more sophisticated than traditional programming language types. For example, instead of just saying “x is a Person,” you can define types like “FatherOf x y” that depend on the specific persons x and y involved.

The key insight is the Curry-Howard correspondence, which establishes a deep connection between mathematical proofs and computer programs. Under this correspondence:

• Types represent propositions (or in this case, queries)
• Terms of a type represent proofs (or witnesses to query results)

This means answering a query becomes equivalent to constructing a mathematical proof, and the proof itself serves as an explanation for the answer.

How It Works: The Obama Family Example

To illustrate DTKGs, the authors use a simple knowledge graph about the Obama family. In traditional RDF, you might write:

ex:Barack rdf:type ex:Person.
ex:Sasha rdf:type ex:Person; ex:father ex:Barack.

In a DTKG using Coq, this becomes:

Inductive Person := barack | michelle | malia | sasha.

Inductive FatherOf : Person -> Person -> Type :=
  | witness_fsb : FatherOf sasha barack.

The first line creates an enumerated type called Person with four members. The second creates a dependent type FatherOf that takes two people as parameters. The witness witness_fsb proves that Sasha's father is Barack.

Direct Queries

To query “Who is Sasha’s father?” you define a record type:

Record FatherSasha :=
  { father : Person; 
    proof_father : FatherOf sasha father }.

This record type has two fields: one for the answer (a Person) and one for proof that this person is indeed Sasha’s father. Answering the query means constructing a term of this type, which Coq can do automatically using tactics:

Theorem sasha_father : FatherSasha.
Proof. 
  eapply Build_FatherSasha. 
  constructor. 
Defined.

The result is:

sasha_father = {| father := barack; proof_father := witness_fsb |}

Notice that the answer includes not just “barack” but also the witness witness_fsb, providing explicit provenance.

Composite Queries

The real power emerges with composite queries that require reasoning across multiple relationships. Suppose the knowledge graph doesn’t directly state that Barack is Malia’s father, but it does contain:

• “Michelle is Malia’s mother”
• “Barack is Michelle’s husband”

In a DTKG, you can define a composite query that deduces the father from these relationships:

Record Father' (x : Person) :=
  { mother' : Mother x; 
    father' :> Husband mother' }.

This encodes the logic: “The husband of x’s mother is x’s father.” When you query for Malia’s father:

Theorem malia_father : Father' malia.

Coq automatically constructs the answer by:

1. Finding that Michelle is Malia’s mother (using witness_mmm)
2. Finding that Barack is Michelle’s husband (using witness_hmb)
3. Combining these to conclude Barack is Malia’s father

The resulting term explicitly shows this chain of reasoning, providing complete transparency about how the answer was derived.

Key Advantages

The research demonstrates three major advantages of DTKGs over traditional knowledge graphs:

1. Compositionality

Queries can be built from simpler subqueries in a modular way. The abstracted query type Father (x : Person) can be reused for any person, and answers from one query can serve as inputs to others. This enables the construction of arbitrarily complex queries from simple building blocks.

2. Explainability

Every answer comes with a witness — a constructive proof of why the answer is correct. For composite queries, the witness explicitly shows the logical chain of reasoning. This is crucial for applications where trustworthiness and auditability matter, such as medical diagnosis, legal reasoning, or financial analysis.

3. Automation

The Coq proof assistant provides tactics that can automatically construct witnesses for queries. The researchers created a custom tactic dqt (DTKG Query Tactic) that can automatically answer many direct queries. Because everything is precisely typed, the system knows which tactics are applicable at each step, enabling significant automation of the query-answering process.

4. Type Safety

Unlike RDF, where type specifications are merely suggestions, DTKGs enforce types at compile time. It’s impossible to create malformed relationships like “Chicago is the father of Barack” — such an attempt would trigger a type error immediately.

Implementation Considerations

The researchers provide an algorithm for converting existing RDF knowledge graphs into DTKGs. The process involves:

1. Converting each RDF class into an enumerated type
2. Converting each RDF property into a dependent type
3. Converting each RDF triple into a term (witness) of the appropriate dependent type

Interestingly, running this conversion algorithm also serves as a validation step: if an RDF graph contains triples that violate its RDFS domain and range specifications, the conversion will fail, revealing data quality issues.

Limitations and Future Work

The paper acknowledges that this is an initial proof of concept. The researchers focused on reproducing the functionality of RDF and SPARQL queries, which represent just the lower layers of the Semantic Web Stack. More sophisticated reasoning capabilities from OWL (Web Ontology Language) and RIF (Rule Interchange Format) remain to be explored.

Other limitations include:

• Learning curve: Dependent type theory is mathematically sophisticated, requiring expertise that many knowledge graph practitioners lack
• Scalability: The paper demonstrates the approach on small examples; scaling to large knowledge graphs (millions or billions of triples) is an open question
• Tool maturity: While proof assistants like Coq are powerful, they’re primarily designed for mathematical theorem proving, not database querying
• Performance: No empirical evaluation of query performance is provided

Broader Implications

This research sits at the intersection of several important trends in computer science:

Formal methods meet AI: As AI systems take on more critical roles in society, the need for verifiable, explainable AI grows. Formal methods from mathematics and computer science offer tools for ensuring correctness and providing explanations.

The explainable AI challenge: Regulators and users increasingly demand that AI systems explain their decisions. DTKGs offer a principled approach to explainability for knowledge-based reasoning.

Semantic web evolution: The Semantic Web vision has been partially realized through knowledge graphs, but challenges around data quality, reasoning, and trust remain. DTKGs suggest a path forward that emphasizes formal rigor.

Proof-relevant mathematics: The paper advocates for proof relevance — the idea that how you prove something matters, not just that you can prove it. In DTKGs, multiple witnesses for the same fact (like different pieces of evidence that Barack is Sasha’s father) are treated as meaningfully different, enabling fine-grained provenance tracking.

Conclusion

Dependently Typed Knowledge Graphs represent an ambitious attempt to bring the rigor of formal mathematics to knowledge representation and reasoning. By treating queries as types and answers as proofs, DTKGs provide built-in explainability and strong guarantees about correctness.

While practical challenges remain — particularly around scalability and accessibility — the approach demonstrates the potential of applying deep theoretical insights to practical problems in AI and data management. As knowledge graphs become increasingly central to AI systems, the need for approaches that ensure correctness and provide explanations will only grow.

The work serves as a proof of concept that may inspire future research at the intersection of formal methods, knowledge representation, and automated reasoning. Whether DTKGs become widely adopted or simply contribute ideas to other approaches, they represent an important step in our ongoing effort to make machines not just knowledgeable, but trustworthy.

About the Research

[embed]Dependently Typed Knowledge Graphs Reasoning over knowledge graphs is traditionally built upon a hierarchy of languages in the Semantic Web Stack…arxiv.org

“Dependently Typed Knowledge Graphs” was authored by Zhangsheng Lai, Aik Beng Ng, Liang Ze Wong, Simon See, and Shaowei Lin, representing NVIDIA AI Technology Centre, Singapore University of Technology and Design, and the Institute of High Performance Computing. The paper was published on arXiv (arXiv:2003.03785v1 [cs.FL]) in March 2020.

More insides in book

[embed]Dependent Types (DTT) & Logic for AI Agent Ready Knowledge Graphs This book explores the intersection of formal logic, type theory, and knowledge representation, arguing for a…leanpub.com

A message from our Founder

Hey, Sunil here. I wanted to take a moment to thank you for reading until the end and for being a part of this community.

Did you know that our team run these publications as a volunteer effort to over 3.5m monthly readers? We don’t receive any funding, we do this to support the community. ❤️

If you want to show some love, please take a moment to follow me on LinkedIn, TikTok, **Instagram. You can also subscribe to our [weekly newsletter](https://newsletter.plainenglish.io/)**.

And before you go, don’t forget to clap and follow the writer️!