A multi-agent framework for distributed theorem proving

In this paper, we explore the possibility of distributed theorem proving using agent-based technologies. We investigate the hyper-linking theorem proving and find out its components which can be performed independently by agents. A multi-agent framework is proposed, wherein distributed theorem proving is achieved by the collaboration of multi-agents each of which performs part of the hyper-linking strategy for completing the proof of the given problems. In this framework, agents communicate with each other via KQML-based messages. Additionally, several system agents are designed for monitoring the traffic and performance of the framework and sharing information. The architecture and the design concepts are addressed. Experimental results show that the proposed framework can effectively perform distributed theorem proving on the Internet.