[過去ﾛｸﾞ] 集合論について (615ﾚｽ)
上下前次1-新
抽出解除 ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
107(6): 2014/02/28(金)02:35 AAS
セマンティクスを使わずに
３つの公理スキーマとＭＰだけを使って
命題論理式の証明を自動で導く
アルゴリズムの名前を教えてください
111: 107 2014/02/28(金)16:34 AAS
スレ違いスンマセン
論理学スレはどれも荒れていて
こちらのスレの雰囲気が良かったので
そういうようなアルゴリズムがあったら教えて
あるいは、関連する研究があったら教えて
という意図での質問でした
誰かしら研究はされてるはずと思っているのですがなかなか見つからない
ゲーデル数を使ったアルゴリズムは読んでいる教科書で軽くスケッチされているけど
細かい部分がよくわからないのでレシピがあったら読みたい
省2
116(2): 107 2014/03/05(水)20:56 AAS
Wang のほうの資料は見つかったけど
同等性のほうの参考文献みつけられません…
同等性はセマンティクスを経由せずに証明できますか？
Deduction Theorem や完全性定理を仮定せずに証明できそうですか？
３つの公理スキーマについては、どの３種類を選ぶかは固定しておりませんが
その手法はそれでも適用できそうですか？
117(4): 107 2014/03/07(金)22:24 AAS
セマンティクスを経由しないでという意味が分かりづらかったので説明します
３つの公理スキーマ
（Ａ１） Ｂ⇒（Ｃ⇒Ｂ）
（Ａ２） （Ｂ⇒（Ｃ⇒Ｄ））⇒（（Ｂ⇒Ｃ）⇒（Ｂ⇒Ｄ））
（Ａ３） （¬Ｃ⇒¬Ｂ）⇒（（¬Ｃ⇒Ｂ）⇒Ｃ）
とＭＰからなる公理系から出発すると、Deduction定理などを経由して完全系定理を示すことができて
この公理系はトートロジーの集合と一致することが示せます
一方、ルカシーヴィッツの公理系
（Ｌ１） （¬Ｂ⇒Ｂ）⇒Ｂ
（Ｌ２） Ｂ⇒（¬Ｂ⇒Ｃ）
省9
119: 107 2014/03/07(金)23:13 AAS
(A1)〜(A3) が定理であることが示せれば
それを使って完全性定理を示せ、
逆に完全性定理を示せるなら
(A1)〜(A3) が定理であることが示せるので、
>118 の条件と >117 の条件は同じ意味になると思います
その >118 での確かめるアルゴリズムがあったらいいのですが…
127(1): 2014/03/08(土)16:26 AAS
>>107と>>117でだいぶ言ってることが違ってる気がするけど。
>>116までを読む限り、公理系が完全なのは前提みたいな書き方だから
2^n通りを虱潰しに調べりゃ良いじゃないか、ということになる。
なんで命題論理の公理図式は一般に3つだと思うようになったのか知らないけど
その体系の公理図式が3つであるのは偶然で、大した意味は無いよ
メレディスの図式みたいに一個からトートロジーを全て導き出せるようなものもある
ウカシェヴィチの公理系から上の三つを頑張って示すか、
ウカシェヴィチの公理系が完全であることの証明が載ってる文献を探すのが一番近道だと思う。
＞ヒラメキなして自動的に判断するアルゴリズムが必要
そんなアルゴリズムあるのかなあ。そもそも無い可能性もある気がするけど。
131: 2014/03/08(土)20:35 AAS
>>127
＞ >>107と>>117でだいぶ言ってることが違ってる気がするけど。
＞ >>116までを読む限り、公理系が完全なのは前提みたいな書き方だから
＞ 2^n通りを虱潰しに調べりゃ良いじゃないか、ということになる。
とすると、>115 のアルゴリズムはまだ自分では把握できていないのですが、
上記のような考え方でのアルゴリズムになるんですかね？
＞ ウカシェヴィチの公理系から上の三つを頑張って示すか、
＞ ウカシェヴィチの公理系が完全であることの証明が載ってる文献を探すのが一番近道だと思う。
確かに目の前のエクササイズの解答を得るにはそれが良さそうですが、それでも
別の ｎ個の公理図式を与えた場合はどうか、また別の…、というふうに
省5
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.217s*