ULKB Logic: A HOL-Based Framework for Reasoning over Knowledge Graphs.

ULKB Logic is an open-source framework written in Python for reasoning over knowledge graphs. It provides an interactive theorem prover-like environment equipped with a higher-order language similar to the one used by HOL Light. The main goal of ULKB Logic is to ease the construction of applications that combine state-of-the-art computational logic tools with the knowledge available in knowledge graphs, such as Wikidata. To this end, the framework provides APIs for fetching statements from SPARQL endpoints and operating over the constructed theories using automated theorem provers and SMT solvers (such as the E prover and Z3). In this paper, we describe the design and implementation of ULKB Logic, its interfaces for querying knowledge graphs and calling external provers, and plans for further development.