改进γ公式的表推演推理方法研究

Tableau Reasoning Method with an Improved γ Formulae

表推演方法是一种接近于逻辑系统表示的自动推理方法,由于其直观性和通用性,易于计算机实现,因此成为目前最普及的自动推理方法之一。在表推演实现时,对γ规则应用次数的限制至关重要,限制次数直接影响表推演的推理效率。给出识别γ公式方法,提出了含γ公式的表推演推理的改进策略,并进行了理论证明和系统实现,该系统与leanTAP软件包进行了对比实验。通过对Pelletier问题的20个实例分析,可以看出γ公式不再需要实例化,大大缩短了表推演的证明过程,减少了搜索空间,提高了推理效率。

Tableau is an automated reasoning method which is closed with Logic system.In implementing tableau it is very important for us to limit the number of γ-rule applications. The number that γ-rule applications affect directly efficiency of tableau reasoning. This paper presents a method for recognizing γ formulae and introduces an improved algorithm for tableau with γ formulae. The system :UniTAP by PROLOG is implemented. Experimental comparisons have been done between UniTAP and leanTAP software package,which is a complete and sound theorem prover for classical first-order logic based on free variable tableaux. By the analyses of 20 of Pelletier's problems, the results show that the instantiations of γ formulae are not taken into consideration. This can be beneficial to yield shorter tableau proofs, and in most cases reduced the search space.