中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
自动演绎中的抽象
作者: 曾云峰
答辩日期: 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)等几种情形,这些证明程序,相对于给定的证明深度都是完全的。最后,我们提出把效能分析作为进一步研究的课题。
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/5614
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
N85505.pdf(2833KB)----限制开放-- 联系获取全文

Recommended Citation:
曾云峰. 自动演绎中的抽象[D]. 中国科学院软件研究所. 中国科学院软件研究所. 1990-01-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[曾云峰]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[曾云峰]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace