Higher Order Semantics and Extensionality. (bibtex)
by Christoph Benzmüller, Chad Brown, Michael Kohlhase
Abstract:
In this paper we re-examine the semantics of classical higher order logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higher order models with respect to various combinations of Boolean extensionality and three forms of functional extensionality. Furthermore, we develop a methodology of abstract consistency methods (by providing the necessary model existence theorems) needed to analyze completeness of (machine-oriented) higher order calculi with respect to these model classes.
Reference:
Higher Order Semantics and Extensionality. (Christoph Benzmüller, Chad Brown, Michael Kohlhase), Technical report, Carnegie Mellon University, Pittsburgh, PA, number CMU-01-03, pp. 1-74, 2003. (Url (preprint): http://christoph-benzmueller.de/papers/R18.pdf)
Bibtex Entry:
@techreport{R18,
  Abstract =	 {In this paper we re-examine the semantics of
                  classical higher order logic with the purpose of
                  clarifying the role of extensionality. To reach this
                  goal, we distinguish nine classes of higher order
                  models with respect to various combinations of
                  Boolean extensionality and three forms of functional
                  extensionality. Furthermore, we develop a
                  methodology of abstract consistency methods (by
                  providing the necessary model existence theorems)
                  needed to analyze completeness of (machine-oriented)
                  higher order calculi with respect to these model
                  classes.},
  Author =	 {Christoph Benzm{\"u}ller and Chad Brown and Michael
                  Kohlhase},
  Institution =	 {Carnegie Mellon University, Pittsburgh, PA},
  Keywords =	 {own, Higher Order Logic, Henkin Semantics, LEO
                  Prover, Automated Reasoning},
  Number =	 {CMU-01-03},
  Pages =	 {1-74},
  Title =	 {Higher Order Semantics and Extensionality.},
  Type =	 {Technical Report},
  Note =	 {Url (preprint):
                  \url{http://christoph-benzmueller.de/papers/R18.pdf}},
  Year =	 2003,
}
Powered by bibtexbrowser