Follow

二分木に要素を追加しても全てのノードのキーが、左の木の全てのノードのキーよりも大きく、右の木の全てのノードのキーよりも小さくなることを証明した。

補題を思い付くのが難しい。たぶん3時間くらいかかった。

gitlab.com/tojoqk/practice-acl

· · Web · 1 · 1 · 3

ACL2 エキスパートになれば、補題とヒントをすぐに思い付けるようになるのだろうか…。もしも、訓練によって補題とヒントがすぐに思い付けるようになったらめっちゃ効率的に証明によってプログラムの信頼性を保証していけるわけなので頑張っていきたい。

Show thread

後からみると10分くらいで思い付きそうなことしかしていないのが悲しい…

Show thread
Sign in to participate in the conversation
Mastodon

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!