7.5 2連結成分アルゴリズム どの1個の頂点を除去しても残りのグラフが連結であるようなグラフグラフを2連結なグラフに分割する。 関節点を見つけるアルゴリズム 深さ優先探索をして、順番をつける。 ある頂点の子孫全てが自分の先祖への逆辺を持っていなけれ…

最汎単一化子 代入の合成 θ=[f(x)/x,g(z,b)/y] σ=[f(z)/x,a/z] h(x,y,z)θσ=h(f(x),g(z,b),z)σ=h(f(f(z)),g(a,b),a) こんな代入になるような代入の合成を定義する。 代入θ=[s1/u1, ... , sm/um],σ=[t1/v1, ... ,tn/vn]に対してその合成は θσ=[s1σ/u1, ... ,sm…

スコーレム標準形 スコーレム標準形とは、存在限量子を含まず、全称限量子の変数が全て異なる冠頭標準形のことである。 スコーレム標準形は任意の論理式に同値な論理式が存在するとは限らないが、任意のAに対してスコーレム標準形Bが存在し、 Aが充足不能 if…