Rule-based Prover Plug-in

hisa (2009年12月 3日 00:47) | コメント(0) | トラックバック(0)

RodinのRule-based Prover Plug-inが公開されていました。

このプラグインではRewrite Rulesの追加ができます。

集合・メタ変数・Rewrite Rulesで定理を構成し、健全性が保たれることの証明を行った上で、その定理を実際のモデルの証明に利用可能になるようです。

まだユーザマニュアルを見ただけで実際には使っていないので、少し使ってみてからまた記事を書きます。