知見

修士論文

置換に関する不動点制約を用いた名目書き換え (新潟大学, 2022.3) [PDF]

名目書き換えシステム (Nominal Rewriting System) という計算モデルのお話です.

ノート

1日1進次郎 (構成的に証明できないトートロジー集) (2020.7.27) [PDF]

2020.7.18 から 2020.7.27 までの10日間で Twitter に毎日投稿し続けた,トートロジーの自然演繹体系での証明木集です.背理法や二重否定の除去などを使わないと証明できない (このことの証明は省略していますが) ものを扱っています.

様相論理の体系と Lindenbaum の補題 (2019.12.14) [PDF]

Mathematical Logic Advent Calendar 2019 の14日目の記事です.様相論理の体系の定義から始まって Lindenbaum の補題を導きます.Axiomatic Extensions の話がメインなので,割とタイトル詐欺です.

ツール

Knuth Bendix Completion in Standard ML [URL]

一階項書き換え系を操作する Standard ML 製の UNIX コマンドです.MLton でコンパイルします.

Brainf*ck in Standard ML [URL]

大学の研究室で Standard ML を使うことになったときに,学習のために作った Brainf*ck のインタプリタです.(100以下の素数を計算するサンプルプログラムを付属しています.)

たんたん洗脳ページ [URL]

担々麺屋さんに行きたくなる洗脳を掛けるページです.Matrix Canvas Code を参考にしました.