Logic in Computer Science (LICS 1997)

Paper: Ramified Higher-Order Unification (at LICS 1997)

Authors: Jean Goubault-Larrecq

Abstract

While unification in the simple theory of types (a.k.a. higher-order logic) is undecidable, we show that unification in the pure ramified theory of types with integer levels is decidable. Since pure ramified type theory is not very expressive, we examine the impure case, which has an undecidable unification problem already at order 2. In impure ramified higher-order logics, expressive predicative second-order subsystems of arithmetic or of inductive theories have concise axiomatisations; because of this and our decidability result for the pure case, we argue that ramified systems are expressive higher-order frameworks in which automated proof search should be practical.

BibTeX

  @InProceedings{GoubaultLarrecq-RamifiedHigherOrder,
    author = 	 {Jean Goubault-Larrecq},
    title = 	 {Ramified Higher-Order Unification},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997},
    year =	 1997,
    editor =	 {Glynn Winskel},
    month =	 {June}, 
    pages =      {410--421},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }