A Mechanization of Strong Kleene Logic for Partial Functions

Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic account of partial functions using three-valued logic decades ago, but there has not been a satisfactory mechanization. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. However, strong Kleene logic, where quantification is restricted and therefore not truth-functional, does not fit the framework directly. We solve this problem by applying recent methods from sorted logics. This paper presents a resolution calculus that combines the proper treatment of partial functions with the efficiency of sorted calculi. Keywords: Partial functions, many-valued logic, order-sorted logic, resolution. This work was supported by the Deutsche Forschungsgemeinschaft (SFB 314) Contents 1 Introduction 3 2 Strong Order-Sorted Kleene Logic (SKL) 4 Syntax : : : : : : : : : :..