计算机应用与软件
計算機應用與軟件
계산궤응용여연건
COMPUTER APPLICATIONS AND SOFTWARE
2007年
8期
14-16,43
,共4页
逻辑系统%定理证明器%形式化方法
邏輯繫統%定理證明器%形式化方法
라집계통%정리증명기%형식화방법
Isabelle是一个通用的定理证明器,应用领域广泛.介绍Isabelle逻辑系统的功能和构成,分析了Isabelle的规格说明语言、验证系统的特点,并给出了用Isabelle逻辑系统来构造Z规格说明的定理证明的方法.
Isabelle是一箇通用的定理證明器,應用領域廣汎.介紹Isabelle邏輯繫統的功能和構成,分析瞭Isabelle的規格說明語言、驗證繫統的特點,併給齣瞭用Isabelle邏輯繫統來構造Z規格說明的定理證明的方法.
Isabelle시일개통용적정리증명기,응용영역엄범.개소Isabelle라집계통적공능화구성,분석료Isabelle적규격설명어언、험증계통적특점,병급출료용Isabelle라집계통래구조Z규격설명적정리증명적방법.
