SAKAI Masahiro - LinearLogic Diff

  • Added parts are displayed like this.
  • Deleted parts are displayed like this.

= 線形論理で使う演算子

書き方をよく忘れてしまうのでメモ。
Unicode, 文字実体参照, ((<TeX>)) での書き方。

* multicative AND
  *「{{e 'otimes'}}」「U+2297」「&otimes;」「\otimes」
  *「{{e '#x2A02'}}」「U+2A02」「\bigotimes」
* multicative OR (‘par’)
  *「{{e '#x214b'}}」「U+214B」「\dnasrepma」
* multicative TRUE
  *「I」
* multicative FALSE
  * 「{{e 'perp'}}」「U+22A5」「&perp;」「\bot」
* additive AND (‘with’)
  * 「&」
* additive OR
  *「{{e 'oplus'}}」「U+2295」「&oplus;」「\oplus」
  *「{{e '#x2A01'}}」「U+2A01」「\bigoplus」
* additive TRUE
  * 「{{e '#x22a4'}}」「U+22A4」「\top」
* additive FALSE
  * 「0」
* linear implication
  *「{{e '#x22b8'}}」「U+22B8」「\multimap」
* !
  * (contraction)
  * "of course"
* ?
  * (weakening)
  * "why not"

= 論理の種類

: ILL
  Intuitionistic Linear Logic.
: MILL
  Multicative Intuitionistic Linear Logic.
  {{e 'otimes'}},1,{{e '#x22B8'}} からなるILLのフラグメント.
: DILL
  Dual Intuitionistic Linear Logic.
#  DILL = MILL + !