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

Preprocess first-order logic formulas for automatic deductions

作　　者：王炜程[1] 刘全[1] 

机构地区：[1]苏州大学计算机科学与技术学院,江苏苏州215006

出　　处：《苏州大学学报（自然科学版）》2009年第2期40-44,共5页Journal of Soochow University(Natural Science Edition)

基　　金：国家自然科学基金资助项目(60673092;60775046;60873116);教育部科学技术研究重点资助项目(207040);中国博士后科研基金资助项目(20060390919);江苏省高校自然科学基金资助项目(06KJB520104)

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

关 键 词：析取范式 否定标准式 斯科伦化 前束范式 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]