中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
程序正确性逻辑验证的一些探讨
作者: 薛涛
答辩日期: 2008-05-29
授予单位: 中国科学院软件研究所
授予地点: 软件研究所
学位: 博士
关键词: 极小一阶逻辑 ; 搜索算法 ; Kripke模型
其他题名: A study on logic method for programme correctness verification
摘要: 搜索算法是逻辑证明中的经典方法,广泛用于直觉主义逻辑,古典逻辑等多种逻辑系统。Kripke模型是一个非常简单而有效的模型,它能对解释直觉主义逻辑的语义给予合理的解释。 本文的主要工作是给出了一个极小一阶逻辑下闭的正公式的搜索算法。该算法基于极小一阶逻辑下闭的正公式证明的可判定性,在[13]的LJB系统中的搜索算法基础上,将[21] 在简单类型理论中的反例构造算法进行拓展,对于任意极小一阶逻辑下闭的正公式,可证的给出证明,不可证的构造一个Kripke模型的反例。随后我们对该算法的正确性以及相关性质给出了证明。
英文摘要: Proof search is a classical method in logic proof. It is widely used in many logic systems, for example, intuitionistic logic and classical logic. Kripke model is a fairly simple and convenient model for the semantics of intuitionistic logic. The main work of this paper is that we present an algorithm of proof search for positive formulas in minimal predicate logic. It is based on the LJB deduction system introduced in [13], and extended the counter model constructing algorithm in simple typed theory in [21] . The algorithm returns a deduction tree, and hence a proof, when the formula is provable, and a Kripke model will be constructed as a counter-model when the formula is unprovable. The soundness and the completeness are proved.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/7254
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_200528015029006薛涛_paper.pdf(515KB)----限制开放-- 联系获取全文

Recommended Citation:
薛涛. 程序正确性逻辑验证的一些探讨[D]. 软件研究所. 中国科学院软件研究所. 2008-05-29.
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