@Article{J5,
  key    =       {J05},
  author =	 {Christoph Benzm{\"u}ller},
  title =	 {Comparing Approaches to Resolution based Higher-Order Theorem Proving},
  journal =	 {Synthese},
  publisher =	 {Springer},
  volume =	 133,
  number =	 {1-2},
  issn =         {0039-7857},
  pages =        {203--235},
  year =	 2002,
  url =		 {www.ags.uni-sb.de/~chris/papers/J5.pdf},
  abstract =	 {We investigate several approaches to resolution based automated theorem
                  proving in classical higher-order logic (based on Church's simply typed
                  lambda calculus) and discuss their requirements with respect to Henkin
                  completeness and full extensionality. In particular we focus on Andrews'
                  higher-order resolution [Andrews71], Huet's constrained resolution
                  [Huet72], higher-order $E$-resolution, and extensional higher-order
                  resolution [BenzmuellerKohlhase98]. With the help of examples we
                  illustrate the parallels and differences of the extensionality treatment
                  of these approaches and demonstrate that extensional higher-order
                  resolution is the sole approach that can completely avoid additional
                  extensionality axioms.},
  note = {doi:10.1023/A:1020840027781},
  chrisnote =	 {J5}
}