"Program development by proof transformation" (Helmut Schwichtenberg)
最小論理(minimal logic)を実装した interactive proof system MINLOG上で、bioinformaticsの定理の自動証明に挑戦する話。
最小論理とは、直観主義論理から矛盾律を除去した体系であり、最小論理における命題の証明は*1λ項によって完全に対応づけられ*2、従って命題は完全に証明項のデータ型であるとみなせる。一方、古典論理上の命題には、最小論理の意味で証明項を持たないものも存在する*3。計算的な視点からは、両者は区別されるべきである。そこで、最小論理で導入できる"computational congtentを持つ"論理結合子は→cと添え字c を付けて表現され、古典論理の論理結合子は→などと添え字なしで表現される。
さて、最小論理の証明はλ項と対応するため、その証明項をscheme上、λ項で表現したのが MINLOG。わかりやすい。MINLOGは、computational contentを持つ（計算的に扱いやすい）推論を扱う。今回の話では、その生命情報学への応用として、組み合わせ論的に膨大な数になりやすい遺伝子の性質を、MINLOG上で証明することに挑戦した。
（後で追記します）
