A Linear Time Algorithm for a Subcase of Second Order Instantiation

  • Donald Simon
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


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 [1] and Huet [2] give semi-decision procedures for finding ω-order unifiers. The second order instantiantion problem is shown to be NP-complete in Baxter [3]. 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.


Constant Function Order Variable Induction Step Type Theory Linear Time Algorithm 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [0]
    T. Pietrzykowski, “A Complete Mechanization of Second Order Type Theory”, (1973), JACM 20, 333–364.MathSciNetCrossRefzbMATHGoogle Scholar
  2. [1]
    D. C. Jensen and T. Pietrzykowski, “Mechanizing ω-Order Type Theory Through Unification”, (1976) Theorectical Computer Science 3, 123–171.MathSciNetCrossRefzbMATHGoogle Scholar
  3. [2]
    G. Hunt, “A Mechanization of Type Theory”, (1975), Theorectical Computer Science 1, 25–58.Google Scholar
  4. [3]
    L. D. Baxter, “The Complexity of Unification,” (1976), Doctoral Thesis, Dept. of Computer Science, University of Waterloo, Waterloo, Ontario.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Donald Simon
    • 1
  1. 1.University of Texas at Austin

Personalised recommendations