Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 07-Oct-2021 18:01:03 JST きゅーけー

   ACL2 はいちおう型なし言語の一つだと思うんだけど、だとしたらすごく面白い話だと思うんだよな。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 07-Oct-2021 18:05:07 JST きゅーけー

     in reply to

     型なしの定理証明支援系で使われてるやつって ACL2 以外にあるんかな。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 07-Oct-2021 18:06:55 JST きゅーけー

     in reply to

     依存型を使った直観主義論理の定理証明支援系は私には合わない感じだった。たぶん、理論的なところじゃなくてインターフェースが悪いんだと思う。

     私は S 式を読むのが得意なので ACL2 と相性がもともと良いんだと思う。