Is it Reasonable to Employ Agents in Theorem Proving?

Christoph Benzmüller, Max Wisniewski— 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

TitelIs it Reasonable to Employ Agents in Theorem Proving?
VerfasserChristoph Benzmüller, Max Wisniewski
ThemaATP, Multi-Agent Systems, Blackboard Architecture, Concurrent Reasoning
Erschienen inIn Proc. of the 8th International Conference on Agents and Artificial Intelligence (ICAART), SciTePress - Digital Library -- Science and Technology Publications, Lda, Vol. 1, 2016.
Größe oder Längepp. 281-286