Experiments on Supporting Interactive Proof Using Resolution

Interactive theorem provers can model complex systems, but require much eort to prove theorems. Resolution theorem provers are automatic and powerful, but they are designed to be used for very dif- ferent applications. This paper reports a series of experiments designed to determine whether resolution can support interactive proof as it is currently done. In particular, we present a sound and practical encoding in rst-order logic of Isabelle's type classes.