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

■

概要

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

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

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

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

■

概要

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

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

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

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

■

概要

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

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

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