Extensional Higher-Order Resolution (bibtex)
by Christoph Benzmüller, Michael Kohlhase
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.
Reference:
Extensional Higher-Order Resolution (Christoph Benzmüller, Michael Kohlhase), In Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings (Claude Kirchner, Hélène Kirchner, eds.), Springer, LNAI, number 1421, pp. 56-71, 1998. (Url (preprint): http://christoph-benzmueller.de/papers/C2.pdf)
Bibtex Entry:
@inproceedings{C2,
  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.},
  Author =	 {Christoph Benzm\"uller and Michael Kohlhase},
  Booktitle =	 {Automated Deduction - CADE-15, 15th International
                  Conference on Automated Deduction, Lindau, Germany,
                  July 5-10, 1998, Proceedings},
  Doi =		 {10.1007/BFb0054248},
  Editor =	 {Claude Kirchner and H{\'e}l{\`e}ne Kirchner},
  Keywords =	 {own, LEO Prover, Higher Order Logic, Automated
                  Reasoning, Henkin Semantics},
  Number =	 1421,
  Pages =	 {56-71},
  Publisher =	 {Springer},
  Series =	 {LNAI},
  Title =	 {Extensional Higher-Order Resolution},
  Note =	 {Url (preprint):
                  \url{http://christoph-benzmueller.de/papers/C2.pdf}},
  Year =	 1998,
}
Powered by bibtexbrowser