Is It Reasonable to Employ Agents in Automated Theorem Proving?

Max Wisniewski, Christoph Benzmüller

2016

Abstract

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.

Paper Citation

in Harvard Style

Wisniewski M. and Benzmüller C. (2016). Is It Reasonable to Employ Agents in Automated Theorem Proving? . In Proceedings of the 8th International Conference on Agents and Artificial Intelligence - Volume 1: ICAART, ISBN 978-989-758-172-4, pages 281-286. DOI: 10.5220/0005824702810286

in Bibtex Style

@conference{icaart16,
author={Max Wisniewski and Christoph Benzmüller},
title={Is It Reasonable to Employ Agents in Automated Theorem Proving?},
booktitle={Proceedings of the 8th International Conference on Agents and Artificial Intelligence - Volume 1: ICAART,},
year={2016},
pages={281-286},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0005824702810286},
isbn={978-989-758-172-4},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 8th International Conference on Agents and Artificial Intelligence - Volume 1: ICAART,
TI - Is It Reasonable to Employ Agents in Automated Theorem Proving?
SN - 978-989-758-172-4
AU - Wisniewski M.
AU - Benzmüller C.
PY - 2016
SP - 281
EP - 286
DO - 10.5220/0005824702810286