@INPROCEEDINGS{C5,
  key    =       {C05},
  AUTHOR =	 {Christoph Benzm{\"u}ller},
  TITLE =	 {Extensional Higher-Order Paramodulation and {RUE}-Resolution},
  YEAR =	 1999,
  BOOKTITLE =	 {Automated Deduction - CADE-16, 16th International Conference
               on Automated Deduction, Trento, Italy, July 7-10, 1999,
               Proceedings},
  EDITOR =	 {Harald Ganzinger},
  PUBLISHER =	 {Springer},
  SERIES =	 {LNCS},
  number =	 1632,
  chrisnote =	 {C5},
  URL =		 {www.ags.uni-sb.de/~chris/papers/C5.pdf},
  PAGES =	 {399--413},
  ABSTRACT =	 {This paper presents two approaches to primitive equality treatment in
                  higher-order (HO) automated theorem proving: a calculus $\EXTPARA$
                  adapting traditional first-order (FO) paramodulation~\cite{RoWo69} , and
                  a calculus $\EXTRUE$ adapting FO RUE-Resolution~\cite{Digricoli79} to HO
                  logic (based on Church's simply typed $\lambda$-calculus). $\EXTPARA$
                  and $\EXTRUE$ extend the extensional HO resolution approach
                  $\EXTRES$~\cite{BenKoh:ehor98}. In order to reach Henkin completeness
                  without the need for additional extensionality axioms both calculi
                  employ new, positive extensionality rules analogously to the respective
                  negative ones provided by $\EXTRES$ that operate on unification
                  constraints. As the extensionality rules have an intrinsic and
                  unavoidable difference-reducing character the HO paramodulation approach
                  looses its pure term-rewriting character. On the other hand examples
                  demonstrate that the extensionality rules harmonise rather well with the
                  difference-reducing HO RUE-resolution idea.}
}