Strategic Principles in the Design of Isabelle
Lawrence Charles Paulson · 2003
Abstract. Interactive proof assistants can support proof strategies, if the right primitives have been included. These include higher-order syntax, logical variables and a choice of search primitives. Such asystem allows experimentation with di erent automatic proof methods, even for constructive logics, new variable-binding operators, etc. The built-in uni cation and search make proof procedures easy to implement, typically using tableau methods. Against subgoals that arise in practice, even straightforward heuristics turn out to be powerful. 1