论文部分内容阅读
搜索算法是逻辑证明中的经典方法,广泛用于直觉主义逻辑,古典逻辑等多种逻辑系统。Kripke模型是一个非常简单而有效的模型,它能对解释直觉主义逻辑的语义给予合理的解释。
本文的主要工作是给出了一个极小—阶逻辑下闭的正公式的搜索算法。该算法基于极小一阶逻辑下闭的正公式证明的可判定性,在[13]的LJB系统中的搜索算法基础上,将[21]在简单类型理论中的反例构造算法进行拓展,对于任意极小—阶逻辑下闭的正公式,可证的给出证明,不可证的构造一个Kripke模型的反例。随后我们对该算法的正确性以及相关性质给出了证明。