An Interactive Driver for Goal-directed Proof Strategies.