JavaScriptのSVGライブラリを探していたら、bonsaiというライブラリが見つかりました。 https://bonsaijs.org/ ロゴもこんな(↓)ですから、これは「盆栽」ですね。Kendo UIというUIライブラリもあるようです。 http://www.telerik.com/kendo-ui Kendo UIのオ…

Isabelleをいじっているあいだ（＝飽きるまで ^^;）は、ダイアリーにIsabelleの話が入るでしょう。今日は小ネタ。「ハイコンテキストな定数・記号の解釈」とかで話題にしたmin-plus半環をIsabelleで書いてみました。あの記事では、通常の演算子記号「+」「*…

昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelle…

以前、証明支援系Coqの記事を書いたことがあります。今日話題にしたいIsabelle（イザベル）は、Coqのライバルと目される証明支援系です。最初のリリースが1986年ですから、実に30年間に渡って開発が続けられています（Coqもほぼ同時期にスタートしています）…