Agent-based Blackboard Architecture for a Higher-Order Theorem Prover
Max Wisniewski, Christoph Benzmüller · 2014
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 prover 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 architectures, 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 implemented a higher-order theorem prover. Eidesstattliche Erklarung Ich versichere hiermit an Eides statt, dass diese Arbeit von niemand anderem als meiner Person verfasst worden ist. Alle verwendeten Hilfsmittel wie Berichte, Bucher, Internetseiten oder ahnliches sind im Literaturverzeichnis angegeben, Zitate aus fremden Arbeiten sind als solche kenntlich gemacht. Die Arbeit wurde bisher in gleicher oder ahnlicher Form keiner anderen Prufungskommission vorgelegt und auch nicht veroffentlicht. Berlin, den (Unterschrift)