-Ants { An open approach at combining Interactive and Automated Theorem Proving
Christoph Benzm, Volker Sorge · 2002
We present the -Ants theorem prover that is built on top of an agent-based command suggestion mechanism. The theorem prover inherits bene cial properties from the underlying suggestion mechanism such as run-time extendibility and resource adaptability. Moreover, it supports the distributed integration of external reasoning systems. We also discuss how the implementation and modeling of a calculus in our agent-based approach can be investigated wrt. the inheritance of properties such as completeness and soundness.