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.

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