| 自动演绎中的抽象 |
| 曾云峰
|
| 1990
|
| 学位授予单位 | 中国科学院软件研究所
|
| 学位 | 博士
|
| 学位授予地点 | 中国科学院软件研究所
|
| 摘要 | 定义了一般合式公式集中纯字的概念，给了纯字规则的非子名形式，合式公式间的一个特殊二元关系。称为涵盖关系（Generalized Subsumption）。并简单讨论了涵盖关系的检验方法。给出了一种删除策略，证明了它的完全性，进而指出，NC归结是广义归结局部地使用删除策略的结果。介绍抽象定理证明的基本思想和基本做法，研究了合式公式集上的一类二元关系，称为NC抽象。指出对任意公式集合S，及任意NC抽象R，如果存在S的NC归结否证T，则必然存在R（S）的NC归结否证T'，且T"的深度不超过T的深度，提出了一种从利用T"构造T的方法，和利用这一方法的一个NC归结证明程序NCPROOF1，NCPROOF1虽然非常有效，但不是完全的。利用部分代换定义WNC归结，并由WNC归结定义WNC抽象。证明了对于一个句子集合S，及WNC抽象R， 对任何S的WNC归结证明T（如果存在的话），必然有R（S）的WNC否证T'，且T'同构于 T。因此，S的NC否证（及WNC否证）的构造完全可以转换成R（S） 的WNC否证空间中的搜索问题，以此为依据，给出了几个证明程序，它们分别包括了只使用一个WNC抽象（WNCPROOF1及NCPROOF2），逐次使用多个WNC抽象（WNCPROOF2 及NCPROOF3），和同时使用多个WNC抽象（WNCPROOF3及NCPROOF4）等几种情形，这些证明程序，相对于给定的证明深度都是完全的。最后，我们提出把效能分析作为进一步研究的课题。 |
| 页数 | 52
|
| 语种 | 中文
|
| 内容类型 | 学位论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/5614
|
| 专题 | 中科院软件所_中科院软件所
|
推荐引用方式
GB/T 7714 |
曾云峰. 自动演绎中的抽象[D]. 中国科学院软件研究所. 中国科学院软件研究所,1990.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论