一阶逻辑公式自动推演前的预处理

Preprocess first-order logic formulas for automatic deductions

讨论了一种方法用于在处理γ子式前先对δ子式进行处理,减少了后期执行的工作量,简化了自动推演程序,并对其在理论上进行了证明,同时也得到了对一阶逻辑公式进行范式转换的方法.

A method which is used to deal with δ clause before the treatment of γ clause is discussed ,the workload is reduced in the late tableau and predigested the automated inference program by using this method. At the same time,we proved it in theory and got a way which convert the original first-order formulas into the normal formulas.