Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction

Shinnosuke Mizutani, Naoki Nishida

A proof tableau of Hoare logic is an annotated program with pre- and post-conditions, which corresponds to an inference tree of Hoare logic. In this paper, we show that a proof tab…