Axiomatization of Typed First-Order Logic

摘要

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.