@InProceedings{C2,
  key    =       {C02},
  author =	 {Christoph Benzm\"uller and Michael Kohlhase},
  title =	 {Extensional Higher-Order Resolution},
  year =	 1998,
  editor =       {Claude Kirchner and H{\'e}l{\`e}ne Kirchner}, 
  booktitle =	{Automated Deduction - CADE-15, 15th International Conference
               on Automated Deduction, Lindau, Germany, July 5-10, 1998,
               Proceedings},
  series =	 {LNAI},
  number =       1421,
  pages =        {56--71},
  publisher =    {Springer},
  chrisnote =	 {C2},
  URL =		 {www.ags.uni-sb.de/~chris/papers/C2.pdf},
  abstract =	 {In this paper we present an extensional higher-order resolution calculus
                  that is complete relative to Henkin model semantics. The treatment of
                  the extensionality principles -- necessary for the completeness result
                  -- by specialized (goal-directed) inference rules is of practical
                  applicability, as an implentation of the calculus in the LEO-System
                  shows. Furthermore, we prove the long-standing conjecture, that it is
                  sufficient to restrict the order of primitive substitutions to the order
                  of input formulae.}
}