On Inductive and Coinductive Proofs via Unfold/Fold Transformations
On Inductive and Coinductive Proofs via Unfold/Fold Transformations
复制标题
DOI：
10.1007/978-3-642-12592-8_7
复制
发表时间：
2009-09
期刊：
影响因子：
--
通讯作者：
H. Seki
中科院分区：
文献类型：
--
作者：
H. Seki
给出了负开折的一个新的应用条件，保证了负开折在分层逻辑程序的开折变换中的安全使用。新的负开折条件是一个自然条件，因为它被认为是替换规则的一个特例。证明了我们的展开/折叠转换系统在完美模型语义意义下的正确性。然后，我们考虑了由Jaffar等人提出的共归纳证明规则。我们表明，我们的展开/折叠变换系统，当使用与Pend-Topor变换，可以证明一个证明问题，这是可证明的共归纳证明规则由Jaffar等人。为此，我们提出了一个新的替换规则，称为soundreplacement，这不一定是等价保持，但是对于执行对应于共归纳的推理步骤是必要的。
We consider a new application condition of negative unfolding, which guarantees its safe use in unfold/fold transformation of stratified logic programs. The new condition of negative unfolding is a natural one, since it is considered as a special case of replacement rule. The correctness of our unfold/fold transformation system in the sense of the perfect model semantics is proved. We then consider the coinductive proof rules proposed by Jaffar et al. We show that our unfold/fold transformation system, when used together with Lloyd-Topor transformation, can prove a proof problem which is provable by the coinductive proof rules by Jaffar et al. To this end, we propose a new replacement rule, calledsoundreplacement, which is not necessarily equivalence-preserving, but is essential to perform a reasoning step corresponding to coinduction.