tag: ACL2
ハフマン符号化して復号すると元に戻ることをACL2で証明した
<2022-07-14 木>
ハフマン符号化して復号すると元に戻ることをACL2で証明しました。全体的に解説は少なめですが、ACL2 の elim ルールについての説明は詳しいと思います。
ACL2 で自然数の和の剰余と剰余同士の和の剰余の等しさを示す
<2022-06-27 月>
ACL2 で剰余関連の証明の試みをしたときの個人的な覚え書きです。
自動定理証明器 ACL2 の入門向けに L-99 の1問目を解きました
<2022-05-25 水>
ACL2 の入門向けに L-99 の一問目を解きました(動画付き)
ACL2 でリストの回文に関する性質を証明した
<2022-04-04 月>
ACL2 で Lisp のリストの回文に関する証明を試みました
ACL2 で鳩の巣の原理を使ってみた
<2022-03-26 土>
ACL2 で鳩の巣の原理を使った証明を試みます
ACL2 でリストの回転に関する性質を証明してみた
<2022-03-24 木>
ACL2 でリストの回転に関する性質を証明してみた(未完)
ACL2 で組み合せの数とその階乗表現の関係について証明してみた
<2021-09-05 日>
ACL2 で再帰で求める組み合せの数と階乗表記の計算方法で計算結果が同じになることを示しました
ACL2 で全ての組み合わせを求める関数の長さの性質について証明してみた
<2021-09-02 木>
全ての組み合せを求めてから長さを求めるのと最初から組み合せの数を求めるので同じ値を得られると証明しました。