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
Is it Reasonable to Employ Agents in Theorem Proving?