2007/07/08

NJEdit

NJEdit 的確好用!以下是 NJEdit 的使用畫面,證明上課給的一個定理 ~~(a | ~a),滿難 XD:

第一張圖和第二張圖 highlight 的 a 是接在一起的,因為框框太小,只好另開視窗 XD。

Max 上課也證過精神相同的定理(還是根本就是同一個?我沒抄下來 XD),即 p 在 classical logic 裡有效(但可能在 intuitionistic logic 裡無效)時,~~p 會在 intuitionistic logic 有效(我說得對嗎?XD)。Max 證完後說這個太難不會考,我自己做一遍後也覺得最好不要考 XD。

--
暫時想不到更短的證明 XD。


It turns out that the proof can be (much) simpler XD. I was obsessed with the thought of using bottom elimination and led myself to a tougher direction. See below for the shorter proof:

另外最新作業 Curry-Howard 的部份我也憑 type system 上課時的印象做了做,不過要等明天上完課才能確切知道 Max 要的是什麼 XD。

--
這樣就不用開兩個視窗,也不用接圖了 XD。

Labels:

Blogger yen37/08/2007 1:15 pm 說:

再放一張結合圖吧XD

 

<< 回到主頁