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.
paper