Profile
Masanori Ogino 𓀁
181351 posts 1993 follows 1215 followers
Please pay attention to random failures.
https://mstdn.maud.io/@omasanori
Masanori Ogino 𓀁 reblogged at 4 years ago
きゅーけー tojoqk@mastodon.tojo.tokyo
ACL2 は定理の証明を自動で探索してくれるんだけど、少し複雑なだけの定理でも普通に失敗する。そこで人間がその定理を ACL2 に解かせるのに必要な補題を考えたり、証明の方向性をミスっているときは ACL2 にヒントを与えてあげたりするのだ。