『線形論理入門 ∼ What’s the USE? ∼』 - pogi-log

『線形論理入門 ∼ What’s the USE? ∼』

照井一成. 線形論理入門 ∼ What’s the USE? ∼. 2003-04-09

線形論理入門 ∼ What’s the USE? ∼

構成的証明

• 式計算においては、証明の単純化＝カット消去手続き

• ゆえに、アルゴリズムの実行＝カット消去手続き

直観主義論理は構成的 (P19)

古典主義論理は非構成的 (P20)

Consumption：線形論理では一度仮定を使うとその仮定は消費される。 (P33)

プルーフネット

自然演繹の線形論理版

#数理論理学