やったこと

ミリ

いちぽむの CD を買ってきた。
個人的にかなり好きな曲なので楽しみ。

日常

なんかメンタルの疲労を感じたので、とりあえず肉でも食べようと思っていきいなりステーキに行った。
注文してから料理が出てくるまでがかなり早くて、いきなりステーキも良くなりつつあるのではないかと実感した。
がんばってほしい。

Presburger

プレスバーガー算術について何となく調べていた。
量化子除去を実装してみたら面白そうだな、と思う。

この辺を参考にしている。

• http://www2.imm.dtu.dk/courses/02917/Presburger1.pdf
• https://gallais.github.io/pdf/presburger10.pdf

実装はとりあえず Scala で。
可能なら Lean とか Idris とか Agda とかで、証明もちゃんと書きたいところ。