2025.11.15
https://gyazo.com/c0ad1412749028ffdf817a96ad9beaf4
キャッシュが一個あたり4GBあってヤバい．これの結果GitHub ActionsのUbuntu Runner上でディスクの空き容量がなくてずっとキャッシュが当たっていなかった． とりあえずこれで空き容量を大きくしたが，なんか本質的にキャッシュ戦略を間違えている気もしなくもない．
連絡
メモ
「2次方程式$ a x^2 + bx + c = 0の解が存在するかどうか」は判別式$ \frac{a \pm \sqrt{4ac - b^2}}{2a}の符号判定によって確認できる． つまり論理式$ \exists x \in \R, ax^2 + bx + c = 0 \iff \lbrack a \neq 0 \land b^2 - 4ac \ge 0 \rbrack \lor \lbrack a = 0 \land (b \neq 0 \lor c = 0) \rbrackであり，
この意味で存在量化子を消せる
このアイデアをもっと応用すると量化子除去のアイデアを得る．