ULKB Logic: A HOL-based framework for reasoning over knowledge graphs

Abstract

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 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). We describe the design and implementation of ULKB Logic, current applications, and plans.