Methods and systems are provided for improved operation of a theorem-proving tool. Logic statements that are to be proved are loaded and a series of interactive commands and assumptions are interactively processed. As the series of commands and assumptions are processed they are tracked. Moreover, the series of commands and assumptions are automatically replayed when a change is received. In some embodiments, the commands are validated for correct syntaxes and data types before the commands are processed.