Extensional Higher-Order Paramodulation and RUE-Resolution (bibtex)
by Christoph Benzmüller
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 \citeRoWo69 , and a calculus $\EXTRUE$ adapting FO RUE-Resolution \citeDigricoli79 to HO logic (based on Church's simply typed $\lambda$-calculus). $\EXTPARA$ and $\EXTRUE$ extend the extensional HO resolution approach $\EXTRES$ \citeBenKoh: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.
Reference:
Extensional Higher-Order Paramodulation and RUE-Resolution (Christoph Benzmüller), In Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings (Harald Ganzinger, ed.), Springer, LNCS, number 1632, pp. 399-413, 1999. (slides) (Url (preprint): http://christoph-benzmueller.de/papers/C5.pdf)
Bibtex Entry:
@inproceedings{C5,
  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.},
  Author =	 {Christoph Benzm{\"u}ller},
  Booktitle =	 {Automated Deduction - CADE-16, 16th International
                  Conference on Automated Deduction, Trento, Italy,
                  July 7-10, 1999, Proceedings},
  Comment =	 {<a
                  href="http://christoph-benzmueller.de//papers/1999-CADE-para-and-rue.pdf">slides</a>},
  Doi =		 {10.1007/3-540-48660-7_39},
  Editor =	 {Harald Ganzinger},
  Number =	 1632,
  Pages =	 {399-413},
  Publisher =	 {Springer},
  Series =	 {LNCS},
  Title =	 {Extensional Higher-Order Paramodulation and
                  {RUE}-Resolution},
  Note =	 {Url (preprint):
                  \url{http://christoph-benzmueller.de/papers/C5.pdf}},
  Year =	 1999,
}
Powered by bibtexbrowser