基于tableau的非经典逻辑经典化的自动定理证明研究

自动定理证明是涉及人类智能问题的重要研究课题之一，对人工智能的研究具有重要的影响和推动作用。本项目针对非经典逻辑缺乏有效的自动定理证明过程的问题，提出将非经典逻辑通过转化，用经典逻辑进行tableau自动定理证明的方法。该方法在经典逻辑的基础上，将逻辑强化学习、归纳逻辑程序设计、布尔剪枝、等式合一、等价翻译等方法应用于非经典逻辑中，使得复杂的非经典逻辑定理可以在经典层面上来证明。一方面，一些提高经典逻辑证明效率的方法，可以应用到非经典逻辑中；另一方面，一些经典逻辑自动定理证明系统只要稍加改动就很容易扩展成为非经典逻辑系统。本项目的研究成果将在符号自动定理证明理论和方法上有所贡献，可以有效地扩大tableau推理的适用范围，在时间和空间上提高证明效率，更大程度地减少tableau扩展的盲目性和不确定性。