SAT for epistemic logic using belief bases

Abstract

In[4] a new epistemic logic LDA of explicit and implicit belief was introduced, and in[5] we presented a tableau-based satisfability checking procedure as well as a dynamic extension for it. Based on such procedure, we created a portable software implementation that works for the family of multi-agent epistemic logics, as well as for the proposed dynamic extension. This software implementation runs as a library for the most common operative systems, also runs in popular IoT and robot hardware, as well as cloud environments and in server-less configurations.