Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 02-Feb-2021 08:52:29 JST きゅーけー

   ついに二分木の探索と二分木を連想リストに変換してから assoc するのが等しいことを証明できたー！！嬉しすぎて泣きそう。ACL2 を使いこなせる気がしてきた。

   https://gitlab.com/tojoqk/practice-acl2/-/blob/3ad5bef9259a2837e25b63dcf8be8d7bee535f1a/binary-tree.lisp#L211

   #ACL2

   • hiromi_mi likes this.
   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 02-Feb-2021 08:57:09 JST きゅーけー

     in reply to

     絶対正しいし必ず証明できると思ってから実際に証明できるまで3日くらいかかってる。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 02-Feb-2021 09:24:57 JST きゅーけー

     in reply to

     証明が終わってから、ACL2 に証明させるには必要のない補題を定義していたことに気づく。必要ないというかむしろ有害な補題だった。https://gitlab.com/tojoqk/practice-acl2/-/commit/c58f7ce61cdf2bbcc86dfd7eb14be7eb31802e6f

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 02-Feb-2021 09:37:01 JST きゅーけー

     in reply to

     絶対正しいだろうけど具体的にどうやって証明したらいいのか見当もつかない状態から、私と ACL2 で S 式によるコミニュケーションを行った結果、定理だと証明できた。これはもう人工知能との対話による定理証明であるといっていいはず。(実際には ACL2 はルールセットを使って証明を探索しているだけだけどね)

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 02-Feb-2021 09:40:07 JST きゅーけー

     in reply to

     定理証明手習いの J-Bob やこの前作った vikalpa (https://mastodon.tojo.tokyo/@tojoqk/105579715190206801) で同じことを証明にようとしたら膨大な時間がかかるはずなので、これでも ACL2 によって得られたものはめちゃくちゃ大きいと言っていいはず。経験を積めばもっと短い時間で証明できるような気もする。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 02-Feb-2021 09:48:04 JST きゅーけー

     in reply to

     ACL2 と「仲良く」なることが重要なわけか。