森岡, 澄夫, 北道, 淳司, 東野, 輝夫, 谷口, 健一
情報処理学会論文誌
36
(10),
2409-2421,
1995-10-15
...提案する証明手順は、制限された記述スタイルのもとで書かれた仕様に対し、構造的帰納法の各段階ごとに、その段階を証明するための武を不変表明などから作り、その式の成立を加減算と比較演算から成る整数上の論理式（プレスブルガー文）の恒真性判定手続きを用いて示す、というものである。従来は、項書き換えや場合分けなどの手法を検証者が複雑に組み合わせて証明していたため、証明に時間がかかり自動化も困難であった。...
情報処理学会
被引用文献6件
参考文献9件
