Distributed modal theorem proving with KE

Abstract

This paper describes an approach to distributed modal theorem proving by bringing together and exploiting two software packages. The first is the implementation of a theorem prover for normal modal logics based on KE and a generalization of Fitting's prefixed tableaux. The second is a library for implementing brokered inter-process communication over the internet. We describe three demonstrators which combine these implementations and illustrate potential applications of the new technology, enabling theorem provers connected to the internet to cooperate, compete, or be used by third parties.