基于矛盾体分离的动态自动演绎推理研究

Logic-based automated deduction reasoning has always been one of the frontier, significant but grand challenge research directions in the research area of logic and reasoning. The proposed research is focused on this research direction. It will draw lessons from and developing our previous research work on α-n(t)-ary resolution-based dynamic automated reasoning theories, methods, algorithms and programs in lattice-valued logic, systematically propose the academic idea of “achieving automated deduction reasoning via contradiction separation in the logical formulae” in the propositional and first-order logic. Hereby this research aims at developing the novel contradiction separation based dynamic automated deduction reasoning theory, establishing the corrsponding novel and effective contradiction separation based sound and complete dynamic automated deduction reasoning methods, as well as designing the corresponding novel automated deduction reasoning system. Preliminary exploration practice has shown and predicted that this line of research will be able to provide a scientific, effective, practical and innovative means for automated deduction reasoning in propositional and first-order logic along with their wide applications.

基于逻辑的自动演绎推理一直是逻辑与推理领域非常前沿、非常重要且非常困难的研究方向之一。本项研究将针对基于逻辑的自动演绎推理，借鉴并发展基于格值逻辑的α-n(t)元归结动态自动演绎推理的理论、方法、算法和程序，分别在命题逻辑和一阶逻辑中系统地提出“通过分离逻辑公式中的矛盾体而实现逻辑演绎推理”的学术思想，以此依次建立基于矛盾体分离的动态自动演绎推理新理论，构建具有可靠性与完备性的基于矛盾体分离的动态自动演绎推理新方法，形成基于矛盾体分离的动态自动演绎推理新系统。初步的探索实践已经说明并预示，这项研究将能为命题逻辑和一阶逻辑中的自动演绎推理及其广泛应用提供一种科学、有效、实用、全新的手段。

本项目针对命题逻辑和一阶逻辑的自动演绎推理，分别提出了基于矛盾体分离的动态多元协同自动演绎推理理论，并刻画了相应的可靠性和完备性，相应地构建了具有可靠性与完备性的基于矛盾体分离的动态多元协同自动演绎推理新方法，进一步建立了基于矛盾体分离的动态多元协同自动演绎推理新算法，并形成了基于矛盾体分离的动态多元协同自动演绎推理新系统，分别形成了命题逻辑Hard问题国际领先的求解器和一阶逻辑国际领先的证明器，分别为命题逻辑公式和一阶逻辑公式的逻辑属性判定提供了有效、可靠、完备的基础工具，并为系统可信性形式化验证提供了必要的手段。