Formalized Formal Logic
Leanによる数理論理学の形式化プロジェクト。Palalansoukîと共同で進めています。 主に様相論理と中間命題論理を担当しており、様々な論理体系やその意味論などを整備したり、無数にある論理体系の分類などを形式化しています。 またその応用として、証明可能性論理の基本定理であるSolovayの算術的完全性定理の形式化も行っています。
数理論理学に興味があります。特にGödelの不完全性定理と様相論理、それらの境界分野としての証明可能性論理について関心があります。
定理証明支援系を用いた数学の形式化に興味があります。特に定理証明支援系としてLeanを用いて数理論理学の形式化を進めています。
Leanによる数理論理学の形式化プロジェクト。Palalansoukîと共同で進めています。 主に様相論理と中間命題論理を担当しており、様々な論理体系やその意味論などを整備したり、無数にある論理体系の分類などを形式化しています。 またその応用として、証明可能性論理の基本定理であるSolovayの算術的完全性定理の形式化も行っています。
色々なWebサービスやWebサイトなどを作ったり、運営したりしています。
開発にはあまり携われていませんが、いくつか機能開発の提案や設計に関する助言をしています。
かつて自分が開発していた音MADのデータベースサイトです。精神的続編としてotoDBになり、今ではソースコードだけが公開された状態になっています。
第200回音MAD晒しイベントで開催される音MADエキスポの公式サイトを作成しました。
観たり、まとめたり、ミックスしたりしています。
モデレータを務めていて、音MADを気が向いたときに登録したりしています。
自分はあまりマイリストにまとめる習慣がなかったので思い出し次第追加し続けています。 投稿日時は無関係であくまでその時期に良かったものです。
ミックスを作ったり、極稀に人前でDJをしたりしています。激しめの音楽にサンプリングの多い曲や音MADでミックスをするのが好きです。 変なDJばかりしていますが要望があれば連絡先からブッキングしてください。
ブレイクコアやハードコア系などのサンプリングの多い激しく速いジャンルに、音MADを混ぜたりして作ったDJミックス集です。
『音MADをテーマにしたDJパーティー』というテーマのイベントに出演します。
(Moe)₂ Chimera Maker™として、DJ DEKAMESHIVIVEとB2BでDJしました。