Christoph Benzmüller
This talk sketches the resource-guided, agent-based suggestion mechanism OANTS for interactive theorem proving and then illustrates how it can be used to build an automated theorem prover or proof planner on top of it. A main benefit of the approach is that it also supports a flexible integration of external reasoning systems and that it can even support cooperative proof constructions among these external systems.