A Linear Time Algorithm for a Subcase of Second Order Instantiation
A problem that comes up in any proof-checking system is whether or not a proof step is a valid instantiation of a lemma or theorem. Often, the lemma or theorem may include set variables and so in general can be second order. This problem is somewhat simpler than the more general problem of second order unification. Jensen and Pietrzykowski  and Huet  give semi-decision procedures for finding ω-order unifiers. The second order instantiantion problem is shown to be NP-complete in Baxter . Our approach will be to find useful subcases of the second order instantiantion problem which yield to fast algorithms. This paper is a first approximation towards that goal.
KeywordsConstant Function Order Variable Induction Step Type Theory Linear Time Algorithm
Unable to display preview. Download preview PDF.