A Mechanization of Strong Kleene Logic for Partial Functions
A Mechanization of Strong Kleene Logic for Partial Functions
复制标题
偏函数的强Kleene逻辑的机械化
DOI：
--
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
M. Kohlhase
中科院分区：
文献类型：
--
作者：
Manfred Kerber;M. Kohlhase
尽管不常被承认，部分函数确实在演绎系统的许多实际应用中发挥着重要作用。 Kleene 几十年前就已经使用三值逻辑给出了偏函数的语义解释，但还没有令人满意的机械化。近年来，人们对多值真值函数逻辑的框架进行了彻底的研究。然而，强克林逻辑（其中量化受到限制，因此不是真值函数）并不直接适合该框架。我们通过应用排序逻辑中的最新方法来解决这个问题。本文提出了一种分解演算，它将部分函数的正确处理与排序演算的效率结合起来。
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.