格值一阶逻辑系统的α广义归结原理

许伟涛,张闻强,徐 扬,张德贤

(1.河南工业大学信息科学与工程学院,河南郑州 450001; 2.西南交通大学数学学院,四川成都 610031)

格值一阶逻辑系统的α广义归结原理

许伟涛1,张闻强1,徐 扬2,张德贤1

(1.河南工业大学信息科学与工程学院,河南郑州 450001; 2.西南交通大学数学学院,四川成都 610031)

在基于格蕴涵代数的格值逻辑系统框架下,笔者扩展了基于格值逻辑系统的α归结原理,将广义子句集上的归结扩展到一般广义子句集上,提出了基于格值一阶逻辑系统LF(X)的α广义归结原理,建立了格值一阶逻辑系统中α广义归结原理的可靠性定理.通过给出的提升引理,证明了该原理的弱完备性定理.这将为建立基于格值逻辑系统的广义归结方法提供新的自动推理技术.

格值一阶逻辑;一般广义子句;局部极复杂广义文字;广义归结;自动推理

自动推理是人工智能领域的重要研究内容.基于归结原理的自动推理是自动推理研究的重要方法. Robinson于1965年提出了基于经典逻辑的归结原理[1],为基于归结原理的自动推理提供了重要的研究基础.之后,自动推理的研究也取得了较多的研究成果[2-9].

基于经典二值逻辑的归结自动推理理论,已形成各种各样的归结自动推理方法,典型的有语义归结、锁归结和线性归结.这些归结方法在证明定理时要将定理的否定写成一阶逻辑中的公式,再把公式化成Skolem标准型,然后将标准型的母式化为合取范式,而合取范式中的每一项都是一个……