Conversation

Notices

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

   #ACL2 以外の他の定理証明支援系も使ってみたい気もするけどなんか直観主義論理だし型で命題を記述する感じなので少しハードルが高い。

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

     in reply to

     あと、ACL2 の勉強は Lisp モチベによって維持されているところがあり、他の定理証明支援系にはそれがないので最初の学習コストの山を乗り越えるのが難しい。