記事一覧
改行が消えているような
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))とか引数をもつ表現まで拡張するところだろうか。
述語論理で書くということ(3)
例3) ボールの運動の述語論理での記述
ここでは運動について考えてみたい。
あるボール(色は白い)が、定規(0から9まで目盛がふってある)の上を運動をすることを考える。
その様子を定規の横に並行に並べられた10台のセンサー(S0からS9と名付ける)で観測する。
動画は扱わなくて、1秒に一回光を当て、センサーはそのときの静止画から、ボールが目盛のどこにあるのかを観測する。
実験の概念図