AboutMe

興味と関心について

お前の好きなものが分かってよかった

次のことに興味が有ります．

Webサービス開発

Webサービス開発に興味があり，個人開発でいくつかのWebサービスを開発しています．またそれらのWebサービスは可能な限りオープンソースで公開することを心がけています． このポリシーは私のように独学でWebサービス開発を学ぶ人の参考になればと思っています．

  1. OtoMADB

数理論理学

論理学一般に関心があります．特に，以下のように述べられるGödel(ゲーデル)の不完全性定理や，その周辺話題におけるパラドキシカルな主張やメタ的な主張が興味深いと思っています．

Gödelの不完全性定理

適当な条件を満たす無矛盾な理論には，証明も反証も不可能な命題が存在する（第1不完全性定理）．更に，その命題は自己の無矛盾性を表す命題と同値である．したがって，自己の無矛盾性を理論自身は証明できない（第2不完全性定理）．

その他にも様相論理にも興味があります．特に様相を理論の証明可能性として解釈することで不完全性定理などを分析する証明可能性論理や，非標準的な様相論理の体系，証明論，計算機科学などのさまざまな分野への応用などにも興味があります．

定理証明支援系

定理証明支援系であり汎用プログラミング言語としても開発されているLeanに興味があります．大規模言語モデルと統合することでLeanでの形式証明の自動生成や証明支援を試みたり，教育支援の場でも用いられているケースがあります．

個人としては，Leanで命題論理や様相論理の種々の話題について形式化を行っていたりしますが，よりもっと使えるケースがあれば使ってみたいとも思っています．

  1. Modal Logic in Lean4

音MAD

観る専門ですが，いつか作ってみたいと思っています．

知識工学

知識の蓄積，整理や検索，またそれらの提示や推薦システムなどに興味があります．

  1. OtoMADB