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

【Abstract】 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.更多还原