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

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