Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 12-Aug-2021 13:55:41 JST きゅーけー

   ACL2 に慣れてきたのでそろそろこれを読む。https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____QUANTIFIER-TUTORIAL

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 12-Aug-2021 14:25:49 JST きゅーけー

     in reply to

     ACL2 では forall とか exists とか使わないで再帰関数に落し込んで証明した方がいいと。自動証明できないんじゃ ACL2 の魅力も半減だし、defun-sk はよっぽどの場合を除いて使わなくてよさそう。https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____QUANTIFIERS