摘要: 本文给出了对框图程序进行形式化的可行算法,并对原有的机械化证明算法作了较大改进,从而提出了三个速证算法。