Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 20:23:38 JST きゅーけー

   加算無限じゃない無限集合に関する定理を Coq とかで証明できるのか気になってる。ACL2 だとまず無理だと思う(無限集合を扱えないので……)

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 20:25:10 JST きゅーけー

     in reply to

     なんか行けそうな記事を見つけた。うーん、こういうのみると ACL2 じゃなくて Coq とか Agda とか使いたくなってくるな……。https://zenn.dev/nyolmol/scraps/d886d52541cac4

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 20:28:27 JST きゅーけー

     in reply to

     あー、無限を扱いたくなると ACL2 じゃ厳しくなってくるんか。私には教官がいないので証明の正しさを確認してくれる人がいないんで定理証明支援系を使いたい気持ちに駆られている。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 20:31:33 JST きゅーけー

     in reply to

     集合の無限分割みたいなことを表現できる定理証明支援系があるなら使いたい。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 20:33:52 JST きゅーけー

     in reply to

     集合の無限分割で検索してもあんまヒットしないんだがなんでだろう。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 20:35:08 JST きゅーけー

     in reply to

     この記事から無限分割の英語版を探して調べるか。https://en.wikipedia.org/wiki/Partition_of_a_set

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 20:40:27 JST きゅーけー

     in reply to

     探し方を間違えてた。これ ZFC をサポートする定理証明支援系を探せばいのか。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 20:43:31 JST きゅーけー

     in reply to

     うー、ACL2 よりも無限集合に対する証明の方がモチベが高くなっていて ACL2 に執着してはならない気がしてきている……。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 20:44:44 JST きゅーけー

     in reply to

     というか実数が扱えるかどうかが気になる。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 20:47:12 JST きゅーけー

     in reply to

     Coq の標準ライブラリに実数があるのか…。https://coq.inria.fr/stdlib/

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 20:47:38 JST きゅーけー

     in reply to

     ACL2 にも ACL2(r) という実数が使えるバージョンがあるらしいしまだ ACL2 の可能性は否定できない。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 20:52:31 JST きゅーけー

     in reply to

     ACL2(r) の詳細について知りたくば論文読めもくは著者に問合せてとのことだった。https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/COMMON-LISP____REAL

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 17-Dec-2021 21:11:39 JST きゅーけー

     in reply to

     Isabelle は ZFC をサポートしてるっぽい記述があるな。