定理証明者の Isabelle に習い始めたのは 2～3 週間ほど前です。私はまだまったくの初心者で、チュートリアル「Isabelle/HOL でのプログラミングと証明」に取り組みました。
これまでに見つけた行列に関する唯一の助けは、HOL ライブラリのソース コードを調べることでした。
次に、行列に関するプロパティを証明する方法を学びたいと思います。行列のラムダ構文は、私にとってまだ新しいものです。Isabelle で行列を使用するためのチュートリアルまたは基本/中間の例はありますか?
1 に答える
5
これは、AFP http://afp.sourceforge.net/entries/Matrix.shtmlの最新のエントリです。
CeTA http://cl-informatik.uibk.ac.at/software/ceta/はアプリケーションとしてここに引用されているので、実際にどのように使用されているかの例を参照できます。
于 2013-05-27T15:01:56.880 に答える