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

Isabelle Tutorial その11

5.7 Interlude: the Basic Methods for Rules 次の規則を例として、メソッドの作用を詳しく見ていきます。 規則の名前をRとします。メソッドruleはQとサブゴールを単一化し、P1からPnを新たなサブゴールとします。メソッドeruleはQとサブゴールを単一化する…