Progress Report on LEO-II -- An Automatic Theorem Prover for Higher-Order Logic
Christoph Benzmüller, Lawrence Charles Paulson, Frank Theiß, Arnaud Fietzke · 2007
Abstract. Leo-II, a resolution based theorem prover for classical higherorder logic, is currently being developed in a one year research project at the University of Cambridge, UK, with support from Saarland University, Germany. We report on the current stage of development of Leo-II. In particular, we sketch some main aspects of Leo-II’s automated proof search procedure, discuss its cooperation with first-order specialist provers, show that Leo-II is also an interactive proof assistant, and explain its shared term data structure and its term indexing mechanism. 1