[過去ﾛｸﾞ]
Inter-universal geometry と ABC予想 49 (1002ﾚｽ)
Inter-universal geometry と ABC予想 49 http://rio2016.5ch.net/test/read.cgi/math/1586650355/
上
下
前次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
抽出解除
必死ﾁｪｯｶｰ(本家)
(べ)
自ID
ﾚｽ栞
あぼーん
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索
歴削→次ｽﾚ
栞削→次ｽﾚ
過去ﾛｸﾞﾒﾆｭｰ
984: １３２人目の素数さん [] 2020/04/15(水) 13:06:47.91 ID:/g+JzMtk >>983 ＞証明支援言語Coqが正しいことを、だれがどうやって保証しているのか？ Coqの正当性をCoqで検証すればいいんじゃね？ http://rio2016.5ch.net/test/read.cgi/math/1586650355/984
985: １３２人目の素数さん [] 2020/04/15(水) 13:10:33.74 ID:/g+JzMtk >>984 具体的に説明するか Coq証明系の存在証明をCoqで書いて プログラムとして抽出すればいいってこと カリー＝ハワード同型対応 https://ja.wikipedia.org/wiki/%E3%82%AB%E3%83%AA%E3%83%BC%EF%BC%9D%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89%E5%90%8C%E5%9E%8B%E5%AF%BE%E5%BF%9C http://rio2016.5ch.net/test/read.cgi/math/1586650355/985
987: １３２人目の素数さん [] 2020/04/15(水) 13:13:33.97 ID:/g+JzMtk >>984 具体的に説明するか Coq証明系の存在証明をCoqで書いて プログラムとして抽出すればいいってこと カリー＝ハワード同型対応 https://ja.wikipedia.org/wiki/%E3%82%AB%E3%83%AA%E3%83%BC%EF%BC%9D%E3%83%8F%E3%83%AF%E3%83%BC%E3%83%89%E5%90%8C%E5%9E%8B%E5%AF%BE%E5%BF%9C http://rio2016.5ch.net/test/read.cgi/math/1586650355/987
988: １３２人目の素数さん [] 2020/04/15(水) 13:15:03.88 ID:/g+JzMtk >>986 抽出されたプログラムにもう一度証明を食わせて 同じプログラムが抽出されればOK http://rio2016.5ch.net/test/read.cgi/math/1586650355/988
992: １３２人目の素数さん [] 2020/04/15(水) 13:25:21.63 ID:/g+JzMtk >>989 漫然とインプットデータといわれても困る 公理や定理の式が正しいとして、証明が間違っていたら？ということはない 公理や定理の式が間違っていたら？ それは検証系で検査できることではない プログラム検証のV&Vで、 後のV(verification 検証)は機械的にできるが 前のV(varidation 妥当性確認）は機械で実施するものではない https://www.ipa.go.jp/files/000036457.pdf http://rio2016.5ch.net/test/read.cgi/math/1586650355/992
994: １３２人目の素数さん [] 2020/04/15(水) 13:27:59.69 ID:/g+JzMtk >>992 誤 varidation 正 validation http://rio2016.5ch.net/test/read.cgi/math/1586650355/994
996: １３２人目の素数さん [] 2020/04/15(水) 13:30:09.19 ID:/g+JzMtk >>993 そもそも、理論として出来上がっているかどうかが疑問視されているなら Coqへの実装は無意味ではないだろう http://rio2016.5ch.net/test/read.cgi/math/1586650355/996
997: １３２人目の素数さん [] 2020/04/15(水) 13:31:03.89 ID:/g+JzMtk >>995 もちろん、すぐにはできないが、やらない言い訳はないな http://rio2016.5ch.net/test/read.cgi/math/1586650355/997
998: １３２人目の素数さん [] 2020/04/15(水) 13:39:57.69 ID:/g+JzMtk >>990 Coqによる検証でも、人間によるテストを全部無くすことはできないが 「人間の証明を、人が再チェックして、確認する」 とかいう機械排除の口実は全く存在しない http://rio2016.5ch.net/test/read.cgi/math/1586650355/998
ﾒﾓ帳
(0/65535文字)
上
下
前次
1-
新
書
関
写
板
覧
索
設
栞
歴
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.040s