![](https://csdnimg.cn/release/download_crawler_static/88626483/bg4.jpg)
A.L. Galdino
,
M.Ayala-Rincón/
电子笔记理论计算机科学
247
(
2009
)
67
导入
results_communication [T]、modulo_equivalence[T]、
results_normal_form[T]、newman_yokouchi[T]
结束
ars
在
ars
理论
中,T被视为一个固定的未解释类型。因此,当
ars
被另一
个理
论
使用时,它必须被实例化。例如,实数的ars
理论
就是
ars[real]。
PVS规范中的一个重要步骤是对建立类型正确性条件TCCs的
理论进行
类型检查,
TCC s是
在理论
可以被认为是类型检查之前必须履行的
证明义务
。TCC的证明可以无
限期地推迟,但只有当证明所依赖的所有TCC和公式都完成时,
理论
才被认为是
完
整的
PVSProver提供了各种命令来构造不同定理的证明。它是交互式使用的,它使用
顺序风格的证明表示来显示正在进行的证明的当前证明目标。证明器维护当前定理
的证明树,用户的目标是构造完整的证明树,在这个意义上,所有的叶子都被识别
为
真。
树的每个节点都是一个证明目标,它是将证明器命令(
规则
或
策略
)应用于
其父节点而产生的。
2.2
基本抽象归约概念的具体化
图1和图2分别说明了
理论
ars
和
理论trs
的
子理论
请注意,
ars
是
trs
的一部分,
图1单独给出只是为了改进表示。
完整的
trs
开发在PVS 4.2中运行,由2745行(82K)和50489行(3.4M)证明
中指定的350个引理组成。PVS建立了124个TCC,其证明包括在后一个数字中。
对应于
理论
ars的
引理的数目是65,其中5个是仅TCC。
理论
ars
进口PVS库的集合
(集
引理),并在此
它建立了形式化ARS定理所必需的二元关系的闭包。假设一个二元关系R在T上,在
PVS中指定为R:VAR
pred[[T,T]]。
它的自反传递闭包RTC(R)是使用
函数
来
指定的,它允许我们获得关于导子长度的归纳证明
RTC(R):
reflexive_transitive
= IUnion(LAMBDA
n:(R,
n))
自反传递闭包的性质的形式化给出为
R_subset_RTC:
LEMMA
子集?(R,RTC(R))
Lemma_RTC:
LEMMA FORALL
n
:
子集?(R,n),
RTC
(R))RTC_幂等
:
LEMMA
RTC(RTC(R))= RTC
(R)
RTC_characterization
:
LEMMA
自反传递?(R)
<=>>最大值
(R = RTC(R))