MiG

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

TitelIs it Reasonable to Employ Agents in Theorem Proving?
VerfasserMax Wisniewski, Christoph Benzmüller
ThemaATP, Multi-Agent Systems, Blackboard Architecture, Concurrent Reasoning
Datum2016
Quelle/n
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