基于广义归结的程序综合

《基于广义归结的程序综合》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、大连理工大学专业学位硕士学位论文基于广义归结的程序综合讯学表插位论文格图个页幅研究生学号研究生姓名刘振晗指导教师评阅人院系主任学位论文完成日期月日大连理工大学,独创性说明作者郑重声明本硕士学位论文是我个人在导师指导下进行的研究工作及取得研究成果。尽我所知,除了文中特别加以标注和致谢的地方外,论文,中不包含其他人己经发表或撰写的研究成果也不包含为获得大连理工大学或者其他单位的学位或证书所使用过的材料。与我一同工作的同志对本研究所做的贡献均。己在论文中做了明确的说明并表示了谢意日期,作者签名甸本壳获`多大连理工大学硕士学位论文摘要自,、动程序设计是计算机科学中的重要研究

2、领域在人工智能的自动规划机器人学。,。等分支有重要应用在程序理论方面程序综合与程序验证关系密切程序综合就是从定理机器证明中抽取程序,即为构造一个符合给定输入输出规范通常表示为一组逻辑,,,公式例如一阶谓词公式的程序首先把程序设计问题转化为定理证明问题然后从定理证明中抽取满足给定规范的程序。,,,对于形如扮又卜夕护仿力的定理证明问题广义归结原理可以回答其是否为真而“万,”,对于对每个确定的夕的值是什么这一经典的证明论问题广义归结原理本身。,并没有给出解答此前很多人研究从归结证明确定夕的值的方法但是由于他们的方法都不是从分析证明过程出发的,所以在很多情况下对问题的解不能

3、做出很好的解释只能完成顺序问题的求解,或者只能列出问题的可能解,却不能回答在任意给定条件下问题的解具体是什。么,,这篇论文主要做了如下两项工作第一对于形如扣无冲肠力的定理证明问物题,本文从分析广义归结证明树的每个结点入手,提取广义归结证明的过程信息,生成问题求解程序。并且给出了所抽取出程序的部分。这一方法的特点是抽取正确性证明、,算法所用的时间空间复杂度与广义归结证明树包含结点数呈线性关系并且抽取算法,。,,,,本身十分简单易于实现第二对于形如物肺护仿夕习的定理证明问题广,义归结证明树中一般包含函数而从这样的广义归结证明树中抽取的程序就可能包含函数。本文给出了是否能

4、够抽取出不包含函数的程序的充分必要,。条件同时给出了消除函数的算法本文给出的算法,主要适用于抽取顺序程序和分支程序,当定理是以递归形式给出,。,。时也可以抽取递归程序利用数学归纳法使用本算法可以抽取循环程序关键词广义归结广义归结证明树定理证明程序综合基于广义归结的程序综合田汕汀,田刃即初滋,盯爪阮斌尔,,即田恤肠,力,州冲行,“,田招,,,认币,,也而,,,认七,认心,,,尸让旧恤肠份力田的刀,成田刀,物卜行,夕,,。幼,由丘而,娜」从七丘,盯访,田认七们,五阶大连理工大学硕士学位论文目录摘要…………绪论……论文的研究背景……相关历史回顾及国内外研究现状……本文的主

5、要研究内容及内容组织……预备知识……一阶谓词演算的基本体系……概述……标准式化简步骤……标准式应用问题……广义归结原理……广义归结原理概述……广义归结方法……广义归结证明树……降低广义归结方法复杂度策略……从广义归结证明树抽取信息……从广义归结证明树抽取信息……抽取算法的正确性证明……函数的消除……应用举例……程序综合……问题求解……结论……参考文献……攻读硕士学位期间发表学术论文情况……基于广义归结的程序综合致谢……︸﹄了︼口大连理工大学学位论文版权使用授权书…大连理工大学硕士学位论文绪论论文的研究背景,。计算机是新技术革命的一支主力也是推动社会向现代化迈进的活跃

6、因素计算机科学与技术是第二次世界大战以来发展最快、影响最为深远的新兴学科之一。计算机产业。己在世界范围内发展成为一种极富生命力的战略产业与此同时,随着社会信息化迅速发展,计算机应用越来越广泛,应用程序开发规模,,。越来越大需求越来越多软件系统日益复杂目前软件生产正面临两个主要问题、,,。、由于开发周期过长且需要长期维护造成非标准化的软件生产开发成本过高。,软件可信赖程度达不到实际要求比如年月的波音飞机撞山失事之,,,后经调查发现失事原因是客机坠毁时关岛国际机场的雷达系统控制软件正出现故,。,障未能在飞机接近地面时及时发出警报年月日阿丽亚娜型火箭第一,。。次鉴定发射因

7、火箭导航系统发生故障而失败两次事故都可以归于软件设计问题目,,。,前在安全要求极高的某些应用领域计算机软件显然无法满足要求更为严重的是,。随着软件复杂性提高和软件应用范围日益拓宽上述两个问题日趋严重高度可靠的软件、无误地完成大型应用软件系统。开发技术需要迅速自从软件危机,。,〔”出现以来寻找类似可靠技术的努力从未终止广义上程序设计被定义为基于不同,,,,知识的推理过程单靠人工完成是不可能不存在错误的因此就需要对软件开发提,。供机,〔〕,器支持或开发基于知识处理和逻辑推理的软件工程工具解决方法之一就是,“”“”。彻底摆脱目前的软件设计模式用做什么型程序代替如何做型