System Description: Proof Planning in Higher-Order Logic with

The Clam system, developed at Edinburgh [4], has been used for several years to develop proof planning, in particular proof plans for induction. An important technique called middle-out reasoning [6] uses meta-variables to stand for some unknown objects in a proof, to be instantiated as the proof proceeds. It has become clear that some domains such as the synthesis and verification of software and hardware systems, and techniques such as proof critics, benefit greatly from middle-out reasoning. Since in these domains the meta-variables often become instantiated with terms of function type, the reasoning is naturally higher-order, and higher-order unification is a vital tool. While some ability to perform higherorder reasoning had been added to Clam in an ad hoc way, it has become clear that it is time to move Clam from first-order to higher-order logic. This system description outlines the Clam system for proof planning in higher-order logic. Clam is written in Prolog [1