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, present its interfaces for querying knowledge graphs and for calling external provers, and discuss a use case of commonsense reasoning in which ULKB Logic is used as the target logic for representing the semantics of English sentences.