Solving for set variables in higher-order theorem proving

Abstract

In higher-order logic, we must consider literals with flexible (set variable) heads. Set variables may be instantiated with logical formulas of arbitrary complexity. An alternative to guessing the logical structures of instantiations for set variables is to solve for sets satisfying constraints. Using the Knaster-Tarski Fixed Point Theorem [15], constraints whose solutions require recursive definitions can be solved as fixed points of monotone set functions. In this paper, we consider an approach to higher-order theorem proving which intertwines conventional theorem proving in the form of mating search with generating and solving set constraints.