解放军理工大学学报（自然科学版）
解放軍理工大學學報（自然科學版）
해방군리공대학학보（자연과학판）
JOURNAL OF PLA UNIVERSITY OF SCIENCE AND TECHNOLOGY(NATURAL SCIENCE EDITION)
2010年
4期
403-407
,共5页
正则表达式%有穷自动机%形式化验证%Isabelle/HOL
正則錶達式%有窮自動機%形式化驗證%Isabelle/HOL
정칙표체식%유궁자동궤%형식화험증%Isabelle/HOL
针对正则表达式和有穷自动机,在机器辅助定理证明系统Isabelle/HOL中进行了形式化描述.通过对语言、正则表达式、确定和不确定有穷自动机在Isabelle/HOL中建立模型,定义了它们之间的相互转换函数并证明了这些函数的正确性,从而验证了正则表达式和有穷自动机在描述能力上的等价性,即:在同一有限字母表下,对任意正则表达式,都存在一个有穷自动机,使得二者描述的语言相同;反之亦然.通过分析与证明,表明采用机器辅助定理证明系统,对计算理论传统核心领域之一的自动机理论进行分析和证明是可行的.
針對正則錶達式和有窮自動機,在機器輔助定理證明繫統Isabelle/HOL中進行瞭形式化描述.通過對語言、正則錶達式、確定和不確定有窮自動機在Isabelle/HOL中建立模型,定義瞭它們之間的相互轉換函數併證明瞭這些函數的正確性,從而驗證瞭正則錶達式和有窮自動機在描述能力上的等價性,即:在同一有限字母錶下,對任意正則錶達式,都存在一箇有窮自動機,使得二者描述的語言相同;反之亦然.通過分析與證明,錶明採用機器輔助定理證明繫統,對計算理論傳統覈心領域之一的自動機理論進行分析和證明是可行的.
침대정칙표체식화유궁자동궤,재궤기보조정리증명계통Isabelle/HOL중진행료형식화묘술.통과대어언、정칙표체식、학정화불학정유궁자동궤재Isabelle/HOL중건립모형,정의료타문지간적상호전환함수병증명료저사함수적정학성,종이험증료정칙표체식화유궁자동궤재묘술능력상적등개성,즉:재동일유한자모표하,대임의정칙표체식,도존재일개유궁자동궤,사득이자묘술적어언상동;반지역연.통과분석여증명,표명채용궤기보조정리증명계통,대계산이론전통핵심영역지일적자동궤이론진행분석화증명시가행적.
