基于语义tableau的一阶逻辑自动定理证明

自动推理作为自动定理证明的扩展是人工智能研究的基础工作,许多重要的人工智能系统都是以推理系统为其核心部分,其中的tableau方法,由于具有通用性、直观性及易于计算机实现等特点,至今成为重要的自动推理方法之一。在tableau方法基础上,讨论了一阶逻辑中的自动定理证明理论,提出使用模型存在定理证明其可靠性和完备性的方法。同时也给出了带等词tableau方法的证明过程。

Automated Theorem Proving Based on Semantic Tableau in First-Order Logic

Automated deduction which is extension to automated theorem proving is a basic work of artificial intelligence.Many important systems of artificial intelligence regard deduction system as core part.Today tableau method has become one of the main deductions,because it is universal and intuitionistic,and easy to be implemented. Based on tableau the theories of automated theorem proving in first-order logic are discussed.For proving the soundness and the completeness,the methods of theorem proving using the model existence theorem are presented.In the mean time,this paper shows proof procedure of tableau with equality.