« 2020年5月 | トップページ

2020年6月22日 (月)

ケネディと天使の問題を Isabelle で証明 その3 悪戦苦闘編

概要


ケネディと天使の問題、または、うそつき天使問題、気まぐれ天使問題、三人の天使問題…と言われているものを、定理証明システム Isabelle でその答えが正しいかチェック(証明)した。

これは「その3」で、気まぐれ天使問題について悪戦苦闘した私の「失敗」を扱う。

続きを読む "ケネディと天使の問題を Isabelle で証明 その3 悪戦苦闘編"

2020-06-22 08:10:47 (JST) in 関数型言語・定理証明器 | | コメント (0)

ケネディと天使の問題を Isabelle で証明 その2 気まぐれ天使問題

概要


ケネディと天使の問題、または、うそつき天使問題、気まぐれ天使問題、三人の天使問題…と言われているものを、定理証明システム Isabelle でその答えが正しいかチェック(証明)した。

これは「その2」で、気まぐれ天使問題を扱う。

続きを読む "ケネディと天使の問題を Isabelle で証明 その2 気まぐれ天使問題"

2020-06-22 08:07:46 (JST) in 関数型言語・定理証明器 | | コメント (0)

ケネディと天使の問題を Isabelle で証明 その1 うそつき天使問題

概要


ケネディと天使の問題、または、うそつき天使問題、気まぐれ天使問題、三人の天使問題…と言われているものを、定理証明システム Isabelle でその答えが正しいかチェック(証明)した。

これは「その1」で、うそつき天使問題を扱う。

続きを読む "ケネディと天使の問題を Isabelle で証明 その1 うそつき天使問題"

2020-06-22 08:02:35 (JST) in 関数型言語・定理証明器 | | コメント (4)