We examine the relationships between axiomatic and cyclic proof systems for the partial and total versions of Hoare logic and those of its dual, known as reverse Hoare logic (or sometimes incorrectness logic). In the axiomatic proof systems for these logics, the proof rules for looping constructs involve an explicit loop invariant, which in the case of the total versions additionally require a well-founded termination measure. In the cyclic systems, these are replaced by rules that simply unroll the loops, together with a principle allowing the formation of cycles in the proof, subject to a global soundness condition that ensures the well-foundedness of the circular reasoning. Interestingly, the cyclic soundness conditions for partial Hoare logic and its reverse are similar and essentially coinductive in character, while those for the total versions are also similar and essentially inductive. We show that these cyclic systems are sound, by direct argument, and relatively complete, by translation from axiomatic to cyclic proofs.

翻译：本文研究了霍尔逻辑及其对偶逻辑（称为逆向霍尔逻辑，有时亦称为不正确性逻辑）在部分正确性与完全正确性版本中的公理化证明系统与循环证明系统之间的关系。在这些逻辑的公理化证明系统中，循环结构的证明规则涉及显式的循环不变式；在完全正确性版本中，该不变式还需额外包含一个良基的终止度量。在循环证明系统中，这些规则被替换为直接展开循环的规则，并辅以一个允许在证明中形成循环的原则，该原则受制于确保循环推理良基性的全局可靠性条件。有趣的是，部分正确性霍尔逻辑及其逆向逻辑的循环可靠性条件在本质上是相似的，且具有共归纳特性；而完全正确性版本的循环可靠性条件同样相似，本质上则具有归纳特性。通过直接论证，我们证明了这些循环系统是可靠的；并通过从公理化证明到循环证明的转换，证明了其相对完备性。