Background on Knowledge Graphs and Types

In this post, Knowledge Graph indicates information stored in a graph-aware database, usually including some ontology features.

Quite often the same knowledge store includes description of space, time, and/or quantitative signal data.  Such hybrid capability suggests a fuzzy boundary between a "knowledge graph" and other flavors of information storage.

Meanwhile Type Theory refers to a vital trend in mathematics and logic towards harmony with concepts that are familiar in computer science.

In this post I provide some general background for discussion of fun ideas at the intersection of
Knowledge Graphs with Type Theory, without delving too far into specific technology issues.

Introductory Material on KGs and KBs

  •  Technically minded may start with this open access e-book  (Springer PDF + HTML), sponsored by European Union project LAMBDA (Learning, Applying, Multiplying Big Data Analytics):
  • The boss's boss may appreciate this glossy, broadly accessible presentation (PDF) from Pool, aka Semantic Web Company (Vienna) :
  • For more depth in applied ontology thinking, check out MK Bergman's work:
    • AI3 blog - outstanding and longstanding
    • KBPedia curated reference ontology (linked below, under example KBs)
    • Bergman's 2018 book A Knowledge Representation Practionary.
  • Engineers interested in RDFS/OWL modeling perspectives should review 

Example Graphs, Datasets, Schemas, and Ontologies

  • Example open access KBs and schema repositories
  •  Example subject ontologies and vocabs, suitable for KG mapping
    • Focused application fields 
    • Broad conceptual fields 
      • Language:  NLP
        • ConceptNet
        • KG-BERT - 2019 paper by Liang Yao, Chengsheng Mao, Yuan Luo
        • Bridges to everything humans describe with words
      • Geography:  GIS
        • Geography and geospatial vocabularies and ontologies are widespread
        • List of ISO standards in digital geography + geomatics, from ISO/TC 211
        • Open Geospatial Consortium - list of open GIS software standards
        • Bridges to earth, ocean, space sciences
      • Humanities:  CIDOC - cultural artifact description, following ISO 21127:2014
        • CIDOC CRM : Conceptual Reference Model, "a formal ontology intended to facilitate the integration, mediation and interchange of heterogeneous cultural heritage information."
    • Most academic fields have ongoing efforts towards standardization of vocabulary, taxonomy, and ontology.  These efforts are important modern manifestations of library science.  

Implementation Patterns for RDF, Gremlin, and other Property Graphs

Here is a taste of active/recent open source KG technology ingredients and design patterns

 Beyond Ontology:  Formal Specification, Proof, and Verification

The connections from assisted theorem proving (ATP) bridge the worlds of  formal mathematics and
digital knowledge science.  Some well-known bridging toolsets are listed below.  As for me, recently
I have been lurching further into the Lean community.  I find it the easiest proof assistant to dabble
in, thanks to a wealth of educational web content.  I also enjoy reading work in Coq and Agda, and experimenting in Idris.   But to keep this reading list short(-ish), we give the most space below to
Lean, which is a CoIC system (calculus of constructions), as are Coq and Agda.   
Here are promised links about the intersection of type models, proofs, and knowledge graphs:

Type Theory meets Semantic Graphs

You guessed it:  Here we are intersecting knowledge graphs with formal types and proofs.

Typed Graph Knowledge - additional conference proceedings, from 2019-20

    Of course, one always finds/re-discovers more and more conferences and sub-conferences.  
    If you have ideas for more links, or other thoughts to share, feel free to reach out on Twizzler: 
    @Stu_B22 or through my biz-card site at

    Popular posts from this blog

    Composed stochastic proof : joint distribution monad as dependent type

    recent work in math knowledge rep 2021Q3

    Domain types based on probability monads