An Efficient Compiler for the IDP-Z3 Knowledge Base System

Knowledge base systems (KBS) store declarative knowledge, on which they can execute different inference tasks, such as “propagation”, which is the derivation of consequences of some given information with respect to the knowledge base. When building larger applications that make use of such a KBS, specific inference tasks are typically invoked through an imperative API. For instance, both the Clasp system for Answer Set Solving and the IDP-Z3 reasoning engine for the FO(·) language offer a Python API for this. However, when the application should be deployed, e.g., in the cloud or on embedded hardware, it is not always convenient or even possible to include the entire KBS as a separate component. For this reason, we investigate the compilation of a knowledge base into a Python program that can perform propagation inference without needing access to an external solver. We investigate this approach for the FO(·) language, presenting and comparing two compilation methods. Experimental results on these two methods demonstrate that high-level propagators achieve better performance than grounded propagators.