補足情報

• [2015/10/22更新, 重要]

  論理式における「括弧」の省略について(論理記号の結合力の強さについて)、 「黒板の体系 (講義での説明)」と、演習システムでの実態 (Coq上の演習シス テムがどう扱っているか)が、食い違っていました。 具体的には、

  • 黒板の体系では、A∧B∧C は (A∧B)∧C の意味(∧は左結合、∨も同じ、⊃のみ右結合)
  • 演習システムは、A∧B∧C は A∧(B∧C) の意味(∧,∨,⊃はすべて右結合)
  となっていました。 これは、非常にわかりにくいので、「すべての論理記号は右結合」と理解して ください。(テキストを、順次改訂します。)

• 計算機室のMacで、バックスラッシュの記号(\)が，「￥」と 表示されているケース [2014/10/9解決済み]
  これは，「ことえり」の環境設定を変更すればよいということを 受講生の１人から教えてもらいました．画面一番上の右端に「ことえりの設定」という ような名前のタブがあるのでクリックして，出てきたウィンドウの下の 方の backslash の表示を変更してください．

• Proof Generalが使えない件 [2014/10/9解決済み]
  以前の演習では、coins計算室の一部の Mac で Proof General がインストール されていない場合がありました。対処済みのはずですが、もし、 自分が使っている coinsマシンにおいて、 /opt/local/share/ProofGeneral/ という directory が 見えなければ、別のマシンを使ってください。

Yukiyoshi Kameyama