2010-04-25から1日間の記事一覧

Isabelle Tutorial その17

6.4 Well-Founded Relations and Induction 整礎性は手続きの停止性と関係します。例えば複雑な再帰関数の定義にはその停止性を保証するための整礎関係を示す必要があり、また多くの数学的帰納法は整礎帰納法の特別な場合です。関係が整礎であるとは、関係が…