Comparing Approaches to Resolution based Higher-Order Theorem Proving (bibtex)
by Christoph Benzmüller
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.
Reference:
Comparing Approaches to Resolution based Higher-Order Theorem Proving (Christoph Benzmüller), In Synthese, volume 133, number 1-2, pp. 203-235, 2002. (Url (preprint): http://christoph-benzmueller.de/papers/J5.pdf)
Bibtex Entry:
@article{J5,
  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.},
  Author =	 {Christoph Benzm{\"u}ller},
  Doi =		 {10.1023/A:1020840027781},
  Issn =	 {0039-7857},
  Journal =	 {Synthese},
  Keywords =	 {own, LEO Prover, Automated Reasoning, Higher Order
                  Logic, Henkin Semantics, ERIH PLUS, History of
                  Logic},
  Number =	 {1-2},
  Pages =	 {203-235},
  Title =	 {Comparing Approaches to Resolution based
                  Higher-Order Theorem Proving},
  Note =	 {Url (preprint):
                  \url{http://christoph-benzmueller.de/papers/J5.pdf}},
  Volume =	 133,
  Year =	 2002,
}
Powered by bibtexbrowser