Axiomatization of Typed First-Order Logic

Reviewed Paper In Proceedings

Author(s):Peter H. Schmitt and Mattias Ulbrich
In:20th International Symposium on Formal Methods (FM 2015)
Series:LNCS
Volume:9109
Year:2015
Pages:470-486
Preprint/PDF:fm2015.pdf
DOI:10.1007/978-3-319-19249-9_29

Abstract

This paper contributes to the theory of typed first-order logic. We present a sound and complete axiomatization for a basic typed logic lifting restrictions imposed by previous results. As a second contribution, this paper provides complete axiomatizations for the type predicates instance_T, exactInstance_T, and functions cast_T indispensable for reasoning about object-oriented programming languages.

BibTeX

@InProceedings{SchmittUlbrich2015,
  author = {Peter H. Schmitt and Mattias Ulbrich},
  title = {Axiomatization of Typed First-Order Logic},
  booktitle = {20th International Symposium on Formal Methods (FM 2015)},
  pages = {470--486},
  year = {2015},
  volume = {9109},
  series = {LNCS},
  doi = {10.1007/978-3-319-19249-9_29},
  month = {jun}
}