### Background on Knowledge Graphs and Types

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

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):
- Knowledge Graphs and Big Data Processing
- E-Published July 2020 by V. Janev, D. Graux, H. Jabeen, E. Sallinger (Eds.)
- The boss's boss may appreciate this glossy, broadly accessible presentation (PDF) from Pool Party.biz, aka Semantic Web Company (Vienna) :
- Knowledge Graph Cookbook by Andreas Blumauer and Helmut Nagy.
- 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
- TOC of Allemang & Hendler
__Semantic Web for the Working Ontologist__, 2nd edition

August update : 3rd edition

### 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
- Finance: FIBO
- Bridges to economics, business
- Biomedicine: OBO Foundry including BFO (Basic Formal Ontology)
- Bridges to chemical sciences, human behavior
- Energy: DABGEO - specification website
- 2020 Paper: "DABGEO ... global energy ontology"
- Astronomy: IVOA vocabularies
- 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

- Graph Storage Patterns
- OBA - Ontology-Based APIs - by Maximiliano Osorio and Daniel Garijo.
- Generates REST OpenAPI service from ontology file
- Straightforward usage of HTTP, JSON, SPARQL
- PGO: Describing Property Graphs in RDF (IEEE open access - PDF
- E-published June-July 2020 by D. Tomaszuk, R. Angles, H. Thakkar
- "Ontology-based approach to transform (automatically) property graphs into RDF graphs."
- TinkerPop - Gremlin integration with RDFS/OWL, SPARQL, SHACL
- Directly Mapping RDF Databases to Property Graph Databases
- SPARQL-Gremlin feature implemented by Gremlinator transpiler
- Match Step in Gremlin 3.x
- AWS Neptune, hybrid RDF + Gremlin, evolved from BlazeGraph
- "Amazon Neptune supports popular graph models Property Graph and W3C's RDF, and their respective query languages Apache TinkerPop Gremlin and SPARQL"
- GUI Patterns
- LODE - Live OWL Documentation Environment
- "a service that automatically extracts classes, object properties, data properties, named individuals, annotation properties, general axioms and namespace declarations from an OWL and OWL2 ontology, and renders them as ordered lists, together with their textual definitions, in a human-readable HTML page designed for browsing and navigation by means of embedded links."
- OpenRefine.org - Pattern-aware dataset mapping, grooming, filtering
- Reconciliation API specification
- Faceted Browsing arch
- Schimatos.org - SHACL-based Web-Form Generator for Knowledge Graph Editing
- Atomgraph projects: LinkedDataHub, Processor, Web-Client .
- Engine Patterns
- SANSA - Large scale semantic analytics incorporating Spark, Flink, ML algos
- Categorized links to many semantic/linked tech resources, curated to be reasonably current

### 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:

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:

- Introductory survey of Type Theory
- Type Theory intro at Stanford Encylopedia of Philosophy
- Links presented with my Scala-DC talk given 2019 October:
- Gitlab-hosted PDF

(Links are clickable when PDF is downloaded, but not in web viewer). - Quick Sampling of formal proof languages and repositories
- Proof Assistant Architectures post by Jiggerwit - brief n' breezy, without links
- Coq - widely used by practicing mathematicians
- Essential theory is CoIC = Calculus of Inductive Constructions
- See Software Foundations free e-book series on verification.
- Agda - gnarly unicode equation civilization of the future, uses CoIC
- cubical agda speaks HoTT truthy terms
- Isabelle and HOL - sensibly incremental, standardized logic engineering
- Uses LF approach, rather than CoIC
- "Logic-Independent Proof Search in Logical Frameworks" by Kohlhase M., Rabe F., Sacerdoti Coen C., Schaefer J.F. (2020)
- Idris - dependent-typing environment, shows Haskell and ML influences
- Metamath - great fun to browse online
- TPTP - Problem Library for Automated Theorem Proving
- Lean is Learnable!
- Learning Lean (by Lean Prover Community)
- Xena Project Blog by Kevin Buzzard
- Natural Number Game
- Made with Lean Game Maker
- Mathlib is growing open lib of lean proofs. Some docs:
- Quick summary of a few core theories, then a meatier undergrad math library
- Broader overview of mathlib, then detailed mathlib docs
- 2020 July - Just a few of the 20+ videos recently posted in youtube: leanprover community
- Infinitude of Primes intro demo - Scott Morrisson Mathematics in Lean intro theory - Patrick Massot
- Building the topological hierarchy - Alex Best
- Category theory - Scott Morrison
- 2018 Review of Lean by Jiggerwit (Thomas Hales) is stimulating ; see also the comments at bottom that page. We may hope that the "steep learning curve" criticism is now addressed by the many resources reachable from the Learning Lean page.
- nLab page on Lean - from category theory perspective
- Tutorial on Design by Contract in Lean, using sorting as example - by Nam Nguyen

### Type Theory meets Semantic Graphs

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

- Papers and Presentations
- Dependently Typed Knowledge Graphs (arXiv:2003.03785)
- 2020 by Zhangsheng Lai, Aik Beng Ng, Liang Ze Wong, Simon See, and Shaowei Lin
- "..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."
- λ-DL and related work at at Uni. Koblenz by Leinberger, Lämmel, Staab et al.
- Type Checking Program Code using SHACL (arXiv:1907.00855)
- 2019 by Martin Leinberger, Philipp Seifer, Claudia Schon, Ralf Lämmel, Steffen Staab
- Lambda-DL project
- 2016 visual slides: Programming with Semantic Broad Data
- 2016 paper: λ-DL: Syntax and Semantics (arXiv:1610.07033)
- LISEQ project - "Language Integrated Semantic Queries"
- "The overall objective of the project is to allow for type-safe programming with graph data. This entails the integration of logics-based data descriptions, in particular DL concepts, into the type checking process of programming lanugages."
- 2016 work by Gabriel Ciobanu, Ross Horne, Vladimiro Sassone
- Introductory Slides - from Ross Horne at U. Luxembourg - SaToSS
- Minimal Type Inference for Linked Data Consumers (ScienceDirect HTML + PDF)
- A Descriptive Type Foundation for RDF Schema (ScienceDirect HTML + PDF)
- Fun slides from Dapoigny, R. and Barlatier, P ca. 2014:
- 2014-5 by Rod Moten
- Modelling the Semantic Web using a Type System (arXiv:1503.01723)

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

- AKBC = Automated
**Knowledge Base Construction** - Accepted conference papers at 2020 AKBC
- AKBC Trip Report from Daniel Daza's blog

- ICJAI = Intntl. Joint Conf. on Artificial Intelligence
- ICCS = Intntl Conf. on
**Conceptual Structures** - IJCAR = Intntl. Joint Conf. on
**Automated Reasoning** - PADL = Practical Aspects of
**Declarative Languages** at Sigplan POPL - 2020 Proceedings (TOC and abstracts, with linked refs)

- CCP =
**Certified Programs and Proofs**, also at Sigplan POPL - 2020 Accepted Papers has TOC with links to pre-prints

- AIKE = Artificial Intelligence and
**Knowledge Engineering** (IEEE International Conference) - 2019 Papers - TOC and abstracts, full-text requires IEEE access

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 Appstract.com

- AKBC = Automated
**Knowledge Base Construction** - Accepted conference papers at 2020 AKBC
- AKBC Trip Report from Daniel Daza's blog
- ICJAI = Intntl. Joint Conf. on Artificial Intelligence
- ICCS = Intntl Conf. on
**Conceptual Structures** - IJCAR = Intntl. Joint Conf. on
**Automated Reasoning** - PADL = Practical Aspects of
**Declarative Languages**at Sigplan POPL - 2020 Proceedings (TOC and abstracts, with linked refs)
- CCP =
**Certified Programs and Proofs**, also at Sigplan POPL - 2020 Accepted Papers has TOC with links to pre-prints
- AIKE = Artificial Intelligence and
**Knowledge Engineering**(IEEE International Conference) - 2019 Papers - TOC and abstracts, full-text requires IEEE access

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 Appstract.com