caeruiro https://blog.hatena.ne.jp/caeruiro/ caeruiro https://caeruiro.hatenadiary.org/ Isabelle 3. More Functional Programming 3.1 Simplification 単純化はIsabelle及び他の多くのシステムにおいて重要な定理証明ツールです。今節では単純化について述べていきます。 3.1.1 What is Simplification? 簡単に言うと、単純化とは等式の左辺から右辺への変換を繰り返すことです。例えば、@のルールを使った単純化のステップを示します。 (0#1#[]) @ [] → 0#((1#[]) @ []) → 0#(1#([] @ [])) → 0#1#[] これは項書換えと見ることもでき、その場合等式は書換規則と見ることができます。… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fcaeruiro.hatenadiary.org%2Fentry%2F20100325%2F1269523782" title="Isabelle Tutorial その6 - caeruiro" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2010-03-25 22:29:42 rich https://caeruiro.hatenadiary.org/entry/20100325/1269523782 1.0 100%