A Breadth-First Strategy for Mating Search

Abstract

Mating search is a very general method for automating proof search; it specifies that one must find a complete mating, without specifying the way in which this is to be achieved. It is the foundation of TPS, an automated theorem-proving system for simply-typed lambda-calculus, and has proven very effective in discovering proofs of higher-order theorems. However, previous implementations of mating search have all relied on essentially the same mating search method: enumerating the paths through a matrix of literals. This is a depth-first strategy which is both computationally expensive and vulnerable to blind alleys in the search space; in addition, the incremental computation of unifiers which is required is, in the higher-order case, very inefficient. We describe a new breadth-first mating search method, called component search, in which matings are constructed by taking unions from a fixed list of smaller matings, whose unifiers are stored and manipulated as directed graphs. Component search is capable of handling much larger search spaces than were possible with path-enumeration search, and has produced fully automatic proofs of a number of interesting theorems which were previously intractable.