| 题名 | 自动演绎中的抽象 |
| 作者 | 曾云峰 |
| 学位类别 | 博士 |
| 答辩日期 | 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）等几种情形，这些证明程序，相对于给定的证明深度都是完全的。最后，我们提出把效能分析作为进一步研究的课题。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 52 |
| 内容类型 | 学位论文 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/5614]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 曾云峰. 自动演绎中的抽象[D]. 中国科学院软件研究所. 中国科学院软件研究所. 1990. |
| 个性服务 |
| 查看访问统计 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论