Iterative Dialogues and Automated Proof

In previous work, we have built a proof system that joins an interactive tactic-based theorem prover for a classical logic with a fully automatic proof planner for a constructive logic. This combined system significantly improves the automation of the interactive prover, but is unsatisfactory for several reasons. To overcome these drawbacks, we propose a general scheme whereby the combined system can pass through multiple rounds of interaction in searching for a proof. This scheme has been implemented and offers an important increase in the power and usability of the combined system.