Semantic Techniques for Cut-Elimination in Higher Order Logic. (bibtex)
by Christoph Benzmüller, Chad Brown, Michael Kohlhase
Abstract:
In this report we present a variety of model existence theorems for classical higher-order logics. The extend the well-known abstract consistency methods to higher-order logics and pinpoint the contribution of extensionality. The results reported here weaken the saturation precondition needed in earlier model existence theorems, making them appliccable to cut-free higher-order logics. This report reprints the article ``Higher Order Semantics and Extensionality'' under review by the Journal of Symbolic Logic and develops the cut-free extensions in detail.
Reference:
Semantic Techniques for Cut-Elimination in Higher Order Logic. (Christoph Benzmüller, Chad Brown, Michael Kohlhase), Technical report, Saarland University, Saarbrücken, Germany and Carnegie Mellon University, Pittsburgh, USA, 2003. (Url (preprint): http://christoph-benzmueller.de/papers/R19.pdf)
Bibtex Entry:
@techreport{R19,
  Abstract =	 {In this report we present a variety of model
                  existence theorems for classical higher-order
                  logics. The extend the well-known abstract
                  consistency methods to higher-order logics and
                  pinpoint the contribution of extensionality. The
                  results reported here weaken the saturation
                  precondition needed in earlier model existence
                  theorems, making them appliccable to cut-free
                  higher-order logics. This report reprints the
                  article ``Higher Order Semantics and
                  Extensionality'' under review by the Journal of
                  Symbolic Logic and develops the cut-free extensions
                  in detail.},
  Author =	 {Christoph Benzm{\"u}ller and Chad Brown and Michael
                  Kohlhase},
  Institution =	 {Saarland University, Saarbr{\"u}cken, Germany and
                  Carnegie Mellon University, Pittsburgh, USA},
  Keywords =	 {own, Higher Order Logic, Henkin Semantics, LEO
                  Prover, Automated Reasoning, Cut-Elimination,R37},
  Title =	 {Semantic Techniques for Cut-Elimination in Higher
                  Order Logic.},
  Note =	 {Url (preprint):
                  \url{http://christoph-benzmueller.de/papers/R19.pdf}},
  Year =	 2003,
}
Powered by bibtexbrowser