Is it Reasonable to Employ Agents in Theorem Proving?

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

Titel
Is it Reasonable to Employ Agents in Theorem Proving?
Schlagwörter
ATP, Multi-Agent Systems, Blackboard Architecture, Concurrent Reasoning
Datum
2016
Quelle/n
Erschienen in
In 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änge
pp. 281-286