| 一阶逻辑公式自动推演前的预处理 |
| |
| 引用本文： | 王炜程,刘全.一阶逻辑公式自动推演前的预处理[J].苏州大学学报(医学版),2009,25(2):40-44. |
| |
| 作者姓名： | 王炜程 刘全 |
| |
| 作者单位： | 苏州大学,计算机科学与技术学院,江苏,苏州,215006
|
| |
| 基金项目： | 国家自然科学基金，教育部科学技术研究重点项目，中国博士后科学基金，江苏省高校自然科学基金 |
| |
| 摘 要： | 讨论了一种方法用于在处理γ子式前先对δ子式进行处理，减少了后期执行的工作量，简化了自动推演程序，并对其在理论上进行了证明，同时也得到了对一阶逻辑公式进行范式转换的方法．
|
| 关 键 词： | 析取范式 否定标准式 斯科伦化 前束范式 |
Preprocess first-order logic formulas for automatic deductions |
| |
| Wang Weicheng,Liu Quan.Preprocess first-order logic formulas for automatic deductions[J].Journal of Suzhou University(Natural Science),2009,25(2):40-44. |
| |
| Authors: | Wang Weicheng Liu Quan |
| |
| Institution: | School of Computer Science and Technology;Suzhou Univ.;Suzhou 215006;China |
| |
| 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. |
| |
| Keywords: | disjunctive normal form negation normal form skolemization prenex form |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
