Agent-based Blackboard Architecture for a Higher-Order Theorem Prover
The automated theorem prover Leo was one of the first systems able to prove theorems in higher-order logic. Since the first version of Leo many other systems emerged and outperformed Leo and its successor Leo-II. The Leo-III project's aim is to develop a new pover reclaiming the lead in the area of higher-order theorem proving.
Current competitive theorem provers sequentially manipulate sets of formulas in a global loop to obtain a proof. Nowadays in almost every area in computer science, concurrent and parallel approaches are increasingly used. Although some research towards parallel theorem proving has been done and even some systems were implemented, most modern theorem provers do not use any form of parallelism.
In this thesis we present an architecture for Leo-III that use parallelism in its very core. To this end an agent-based blackboard architecture is employed. Agents denote independent programs which can act on their own. In comparison to classical theorem prover archiectures, the global loop is broken down to a set of tasks that can be computed in parallel. The results produced by all agents will be stored in a blackboard, a globally shared datastructure, thus visible to all other agents. For a proof of concept example agents are given demonstrating an agent-based approach can be used to implement a higher-order theorem prover.