Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 22-Mar-2022 12:12:02 JST きゅーけー

   なんか色々考えた結果、ACL2 を再びやろうという謎の結論に至った(極端)

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 22-Mar-2022 12:12:43 JST きゅーけー

     in reply to

     ACL2 は簡単な関数の簡単な定理を証明している限りは楽しいんだよな。難しいやつは消去バーストが長く続かないと無理。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 22-Mar-2022 12:13:39 JST きゅーけー

     in reply to

     LISP-99 にでてくる最初の方の関数はとりあえず簡単な関数でそれに関連する定理も割と簡単に証明できるんだよな。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 22-Mar-2022 12:14:11 JST きゅーけー

     in reply to

     まだ最初の 21 問しか解いてないのでいつから難しくなるのか分からん。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Tuesday, 22-Mar-2022 12:20:20 JST きゅーけー

     in reply to

     L-99 の P23、乱数必要じゃん。これは死んだ。