記事一覧
矛盾から任意の論理式が証明できる件
ワタシは論理学の専門家ではありませんが、論理学は面白いのでいろいろ考えたりします。矛盾からは任意の論理式が証明できるという、直感的にあやしいことがらについて、すこし考えたので書いておきます。
Gentzen(G)系は推論規則の、Hilbert(H)系は数学の議論の研究が目的のようだ。
論理には、定義/公理と推論規則の二つの部分がある。
Gでは、公理はA⇛A(スキーマとかシェーマと呼ばれるやつ
unificationを書いてみる(1)
表現を書く
unificationを書きたいのだけど、unificationという理解だと、どうしても手続きになってしまう。
最初は仕方がないと思う。
いろいろやってみたけど、なんか間違っているような気もする・・・
一番簡単な項として、定数aを考えてみる。
項がaだけのclauseの集合Σがあったとする。このときのDの定義はどうなるだろうか。
まず、項というより、表現(Expr)を定義して
改行が消えているような
noteにテキストをコピペすると、改行が無視されて全部くっついてしまう。
かと思えば、文章の塊は空行でブロックに分けられる。
つらい
中央公園(20240109-20240209)
真夜中に中央公園を通り抜けようと考えたのはなぜだったろうか。
深夜でも公園は取り囲まれているビルの灯りで隅々まで見通せる。タチの悪い乱暴者が潜んで いればすぐにわかるはずだ。それでも、夜の闇の塊はあちらこちらにおちているだろう。そんな公 園を誰が通り抜けようとしたのだろうか。
真夜中に中央公園を通り抜けていったのは誰だろう。
それは公園の向こう側にある託児所に預けていた子供を引き取りに行こうと
Unificationアルゴリズムにも迷う
Unificationは2つの式(論理式や項)から、代入mguを計算するアルゴリズムである。
以下に示す例では、x, y, zは変数、a, b, cは定数、f, g, kは関数記号とする。
2つの式とmguの例)
t1,t2 を式として、<t1:t2>でunificationした結果のmguを表す。
(1) <a : b> : unifyできない
(2) <f(a) : g(b,c)>
resolution(述語論理)
矛盾については命題論理だけで話ができた。
ここでは、述語論理のresolutionについてまとめたい。
命題論理のresolutionでそうだったように、2つのclausesからresolventを作るという形式は述語論理でも変わらない。
見た目の違いといえば、命題論理ではPとかQとか書いていたことを、述語論理ではP(x,y)とかQ(f(a))とか引数をもつ表現まで拡張するところだろうか。