A first order logic for partial functions

AbstractPartial functions are the most suitable characterization of program effects. Formal reasoning on programs should be supported by logics dealing with partial functions. In this paper, we present a first order, three valued logic for partial functions, together with a semantical motivation of its model theory. We also present a calculus for the logic, proving its soundness and completeness. The calculus is introduced together with a methodology for building calculi for logics involving partial functions