tag: ACL2

ハフマン符号化して復号すると元に戻ることをACL2で証明した

<2022-07-14 木>

ハフマン符号化して復号すると元に戻ることをACL2で証明しました。全体的に解説は少なめですが、ACL2 の elim ルールについての説明は詳しいと思います。

<2022-06-27 月>

ACL2 で剰余関連の証明の試みをしたときの個人的な覚え書きです。

<2022-05-25 水>

ACL2 の入門向けに L-99 の一問目を解きました(動画付き)

<2022-04-04 月>

ACL2 で Lisp のリストの回文に関する証明を試みました

<2022-03-26 土>

ACL2 で鳩の巣の原理を使った証明を試みます

<2022-03-24 木>

ACL2 でリストの回転に関する性質を証明してみた(未完)

<2021-09-05 日>

ACL2 で再帰で求める組み合せの数と階乗表記の計算方法で計算結果が同じになることを示しました

<2021-09-02 木>

全ての組み合せを求めてから長さを求めるのと最初から組み合せの数を求めるので同じ値を得られると証明しました。