Springe direkt zu Inhalt

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

Is it Reasonable to Employ Agents in Theorem Proving?
ATP, Multi-Agent Systems, Blackboard Architecture, Concurrent Reasoning
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