Twelf Dependent Types and Logic for Knowledge Graph and Ontology Description