A first order logic for partial functions (Q918965)

A major aim of this paper is to clarify the semantic possibilities for logics dealing with partial functions which should support the formal reasoning on programs. The authors present a first order, three valued logic for partial functions named PFOL, together with a semantical motivation of its model theory. The main difference between PFOL and traditional first order logic is in allowing partial predicates and partial functions. In the rest of the paper they show how to obtain a sound and complete sequent calculus by applying the Beth's tableaux method.