Is It Reasonable to Employ Agents in Automated Theorem Proving?
Max Wisniewski, Christoph Benzmüller · 2016
Agent architectures and parallelization are, with a few exceptions, rarely to encounter in traditional automated theorem proving systems. This situation is motivating our ongoing work in the higher-order theorem prover Leo-III . In contrast to its predecessor – the well established prover LEO-II – and most other modern provers, Leo-III is designed from the very beginning for concurrent proof search. The prover features a multiagent blackboard architecture for reasoning agents to cooperate and to parallelize proof construction on the term, clause and search level.