Home | Notifications | New Note | Local Timeline | Federated Timeline | Profile | Logout
きゅーけー@tojoqk@mastodon.tojo.tokyo(2025-12-03 21:55:32) PAIPの日本語訳の実用Common Lispをペラペラと呼んでいた結果、いま自分がACL2を使って定理証明をしているのはかつてのAI研究の成果を享受しているのだということがわかった。 Reply
---Replies---
きゅーけー@tojoqk@mastodon.tojo.tokyo(2025-12-03 21:57:40) ACL2がいろんなヒューリスティックを駆使して自動で定理証明するのはまさに実用Common Lispに書いてあるヒューリスティックな探索の話に通じるように思う。