Higher-Order Proof by Consistency
We investigate an integration of the first-order method of proof by consistency (PBC), also known as term rewriting induction, into theorem proving in higher-order specifications. PBC may be seen as well-founded induction over an ordering which contains the rewrite relation, and in this paper we extend this method to the higher-order rewrite relation due to Nipkow. This yields a proof procedure which has several advantages over conventional induction. First, it is less control demanding; second, it is more flexible in the sense that it does not instantiate variables precisely with every constructor, but instantiates according to the rewrite rules. We show how a number of technical problems can be solved in order for this integration to work, and point out some desirable refinements that involve challenging problems.