@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}
}
Axiomatization of Typed First-Order Logic
| Autor(en): | Peter H. Schmitt und Mattias Ulbrich |
|---|---|
| In: | 20th International Symposium on Formal Methods (FM 2015) |
| Reihe: | LNCS |
| Band: | 9109 |
| Jahr: | 2015 |
| Seiten: | 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.