proof assistants

1. basic idea

You have a proof goal and a set of assumptions. You need to move your proof state to the proof goal. You do this interactively using tactics.