Masaki Hara

ややマニアックですが、論理学の問題を解くtwitter botです。 正確に言うと、直観主義命題論理と呼ばれる種類の問題を解きます。これは高校数学で出てくる論理と集合のものとよく似ていますが、以下のような違いがあります。 ・排中律「Aまたはnot A」が成り立たないという特殊な仮定をおくこと ・全ての代入を試すことで証明する手法が困難であること ・計算量的には、古典論理のそれがco-NP完全なのに対して、直観主義の場合はPSPACE完全であること アルゴリズムはHudelmaierによって提案されたO(n log n)空間のものを用いています。これに加えて、証明を正規化されたNJに整えて出力する機能と、正しくなかった場合にKripke意味論での反駁を提示する機能を供えています。