日々の流転

λ. ETでワンのアルゴリズムを……挫折

せっかくだから、あろは先生を問い詰める会の前にETと「搾り出し方」を試してみるかと思い、昔Haskellで書いて微妙だった Wang's Algorithm (ワンのアルゴリズム) を試してみることにする。

仕様

仕様は以下の組 (D,Q) で表される。

1. ホーン節で書かれた背景知識 D
2. ホーン節で書かれたクエリーの集合 Q

まずは背景知識D。これは実行可能性は考えなくて良いはずなので、まあ適当にアルゴリズムではなく定義っぽい感じで。

valid(X) ← valid([], [X]).

valid(Gamma, Delta)) ← member(X, Gamma), member(X, Delta).
valid(Gamma, Delta) ←
  permutation(Gamma, Gamma1), valid(Gamma1, Delta).
valid(Gamma, Delta) ←
  permutation(Delta, Delta1), valid(Gamma, Delta1).

valid(Gamma, [and(A,B)|Delta])) ←
  valid(Gamma, [A|Delta]), valid(Gamma, [B|Delta]).
valid(Gamma, [or(A,B)|Delta])) ← valid(Gamma, [A,B|Delta]).
valid(Gamma, [not(A)|Delta])) ← valid([A|Gamma], Delta).
valid([and(A,B)|Gamma, Delta)) ← valid([A,B|Gamma], Delta).
valid([or(A,B)|Gamma], Delta)) ←
  valid([A|Gamma], Delta), valid([B|Gamma], Delta).
valid([not(A)|Gamma, Delta)) ← valid(Gamma, [A|Delta]).

valid(Gamma, [imply(A,B)|Delta]) ← valid(Gamma, [or(not(A),B)|Delta]).
valid([imply(A,B)|Gamma], Delta) ← valid([or(not(A),B)|Gamma], Delta).

member(X, [X|_]).
member(X, [_|T]) ← member(X,T).

permutation([], []).
permutation(L, [X|L2]) ←
  select(X, L, L1),
  permutation(L1, L2).

select(X, [X|L], L).
select(X, [Y|L], [Y|L1]) ← select(X, L, L1).

お次はクエリーの集合Q。

prb1

ans(X) ← valid(X).

prb2

s ← valid(imply(imply(a,b), imply(imply(a,imply(b,c)), imply(a,c)))).

prb3

k ← valid(imply(a, imply(b, a))).

prb4

peirce ← valid(imply(imply(imply(p, q), p), p)).

Q = {prb1, prb2, prb3, prb4}

処理系のダウンロード

<URL:http://assam.cims.hokudai.ac.jp/et/indexj.html>

搾り出し方

早速、論文の手順に基づいて搾り出してやるぜ!　と思って喜び勇んではじめたら、肝心のパターンの決定とルールの生成の部分がこの論文には書いていないのだった。しょぼーん。

もちろん、アルゴリズムを直接書くのは難しくないと思うけど、それをETでやっても仕方がないと思うし。