論理計算の線形代数化について

論理計算の線形代数化について

Embedding Tarskian semantics into linear spaces

佐藤泰介

12∗

1

_{国立研究開発法人産業技術総合研究所人工知能研究センター}

2

_{国立情報学研究所}

Abstract: We propose a new linear algebraic approach to the computation of Tarskian semantics in logic. We embed a finite model M with N entities for a language of first-order logic in N-dimensional Euclidean spaceRN by mapping entities of M to N dimensional one-hot vectors and k-ary relations to order-k adja-cency tensors (multi-way arrays). Second given a logical formula F in prenex normal form, we compile F into a setΣF of algebraic formulas in multilinear algebra with a nonlinear operation. In this compilation,

when existential quantifiers quantify two occurrences of a variable, they are compiled into identity matri-ces. It is shown that a systematic evaluation ofΣF inRN gives the truth value, 1(true) or 0(false), of F in

M. We also discuss the effect of low-dimensional embedding of M using bilinear models where existential quantifiers are compiled into non-identity matrices.

1

はじめに

近年 wikipedia などの知識資源の発展とともに YAGO[12], Freebase[1], Knowledge Vault[2]などの巨大な knowl-edge graph(KG,知識グラフ) が出現しつつある。KG は一 般に主語 (subject, s)、述語 (predicate, p)、目的語 (object, o) の３つ組 (s, p, o) の集合を node s と o を関係 p で結 んだグラフとして表現したものである。例えば３つ組 (Obama,birthplace,Hawaii)は米国大統領の Barack Obama の出生地 (birthplace) がハワイであることを表す。この ような３つ組の集合はネットワーク時代の集合知を表 す knowledge base(KB, 知識ベース) として、将来の AI 技術の infrastructure を成すと考えられる。KG の現状 については Nickel et al.[8] で総合的な解説がなされて いる。 KGは論理学から見ると ground atom からなる単純な 命題データベースであるが、KG に対する演繹 (deduc-tion)、発想 (abduction)、帰納 (induction) などの論理推 論の取り組みは初歩的段階に留まっている。伝統的にこ のような命題データベースに対する QA は記号的な論理 推論の枠組みで成されて来た。しかし計算量の観点から して記号的 approach は scale せず big data 時代の論理推 論を担うことは難しい。また MLN のような判別的確率 モデルも計算量の問題を抱えている。一方 Knowledge Vault[2]に見られるように explict feature もしくは latent featureを使った実数による (近似的) 論理推論は Web レ

∗_{連 絡 先：国 立 研 究 開 発 法 人 産 業 技 術 総 合 研 究 所 人 工}

知 能 研 究 セ ン タ ー (〒 135-0064 江 東 区 東 区 青 海 2-3-26) E-mail:[email protected]

ベルで scale する。例えば RESCAL[9, 7]1の bilinear2 modelは latent feature に基づくが、そこでは内積など 単純な線形代数の実数演算のみが使われ、２引数述語

r(x, y)は関係を表す行列 R と entity を表すベクトルに x, yにより (x•Ry) = xTRy = R•1x•2yとしてテンソル

表現される。ここで x, y や R は低次元の線形空間に埋 め込まれており、alternating least squares(ALS) 法によ り効率よく KG から学習される [8]。KG は ground atom に限るとは言え、従来の記号的論理推論に対し (多重) 線形代数に基づいた実数による論理推論という新しい 視点と課題を提供していると言える。

2

課題：

Tarskian sematics

の線形代

数化とその応用

KGは各分野で bottom-up に発展した来たものであり、 Semantic Webの RDF、情報抽出の relation extraction、 NLPの vector-based な computational semantics、あるい は DNN の NTN や RNTN など様々な分野の研究と交差 している。しかしながら KG が命題の集合であり、論 理学の対象でもあるということは必ずしも強く意識さ れていない。論理学から見て述語論理の意味論である モデル論の線形代数による計算と見なせる研究が既に 幾つかあるものの [4, 10, 11, 6, 13]、empirical で部分的 1_{RESCALは scikit-tensor(https://github.com/mnick/scikit-tensor) に} 含まれている。scikit-tensor は python で書かれたソフトウェアで、 RESCALの他、 Canonical/Parafac Decomposition、Tucker Decompo-sition、DEDICOM、INDSCAL の機能を提供している。 2_{写像 f (x, y) が f (cx} 1+ x2, y) = c f (x1, y) + f (x2, y), f (x, cy1+ y2) = c f (x, y1) + f (x, y2)を満たすとき f (·,·) を biliear(双線形) と言う。 人工知能学会研究会資料 SIG-FPAI-504-03

な研究が大部分で、論理の一貫した線形代数的取り扱 いには至っていない。 我々は big data 時代の AI の技術的基礎として、一階 述語論理の標準的意味論である Tarskian semantics の多 重線形代数化 (テンソル化) とそれにもとづく各種の論 理推論を効率的に且つ scalable に実現したい。そのた め具体的に以下の各項目について研究を行う必要があ ると考える。 • Tarskian semantics の線形代数的形式化 • 演繹、発想、帰納の各種推論の線形代数的実現 • 並列化による高速推論法の開発と実装 • 低次元空間埋め込みによる近似推論法の開発と 実装 • 応用 まず AI の知識表現の理論的な面から言うと、今まで手 が付けられていなかった限量子 (quantifier) のテンソル 化が重要である。我々はモデル M 上の限量子を含む任 意の論理式の真偽値をべクトル、行列、テンソルなど を使って compositional に且つ厳密にあるいは近似的に 計算する方法を得たい。関連してモデル M 上の演繹、 発想、帰納の各推論の線形空間に於ける定式化は自明 ではないので、(従来の証明論を使った記号的定義とは 独立に) 新に定式化する必要がある。 具体的な計算法と実装の観点から見ると、まず並列 化の可能性が着目される。行列による線形代数計算は 並列化による最適化のチャンスが多く、最新の計算機 パワーを活かした many core, GPGPU を使った並列計 算が期待できる。更に行列計算は原則データサイズの 多項式オーダの計算量であるという好ましい性質も備 えているので、brute force による大量計算も視野に入 れるべきである。 論理の線形代数化に於ける最も興味深く、実用的に 重要な課題は低次元空間埋め込みによる近似推論法の 開発と実装であろう。記号的 approach では不可能な近 似が容易に線形空間で可能である。記号 approach では 困難であった並列化と近似の容易さが線形代数的論理 計算の大いなる利点と考えられる。 応用としては、KG を含む実 data 上の各種論理推論 が当面の目標である。現状の KG では（それ自体は全く 演繹的推論ではない）関係の連鎖を辿ると言う演繹推 論に似た操作が実現されているに過ぎない。また帰納 推論については KG に内在する一般的規則性を definite clauseの形で論理式として抽出する試みが幾つかある ものの [3, 5, 13]、発想推論は全く手付かずである。発 想推論は観測事象に対する最適な説明を求めるもので あり、結果を導く未観測の原因を推論するものとして 実用的に重要な推論形式である。 本論文では以上述べた研究課題の中で「Tarskian se-manticsの限量子を含む線形代数的形式化」の部分につ いて一つの形式化の試みを報告する。関係データベー スの論理的一般化である Datalog   program の線形代 数的評価法や線形代数的な発想推論の実現などについ ては、紙面の都合上別の機会に報告したい。

3

隣接行列と

one-hot encoding

によ

る

Tarskian semantics

の線形代数

表現

Tarskian semanticsの線形代数化の第一歩は、モデル Mの領域 (domain) の個体 (entity) とその上の関係 (rela-tion)を線形空間に map することである。有限 Herbrand 領域の 2 項関係のみを扱い、論理式は等号も関数記号も 含まないものとする。以下概略を説明する。モデル M の領域をD = {e1, . . . , eN}、その上の 2 項関係を r(x,y) とする。まず個体 ei(1≤ i ≤ N) は one-hot encoding に より i 番目の成分だけが 1 で、後は全部 0 であるベク トル ei= [0···1···0]T に map する。 D 上の２項関係 r(·,·) を i j 成分が ri j= { 1 if M|= r(ei, ej) 0 それ以外 であるような N× N 行列 R により表す。すると素式 r(ei, ej)の M に於ける真偽値を [[r(ei, ej)]]∈ {1(真),0(偽)} と置くと、[[r(ei, ej)]]は [[r(ei, ej)]] = eiTRej = (ei• Rej) (1) により行列演算で計算される。R を関係 r を表現する 行列と呼ぶ。r(x, y) の引数を入れ替えた述語 r′(x, y) = r(y, x)は転置行列 RT により表現される。 M上の論理式 F の真偽値 [[F]] を与える (1) の右辺の ような線形代数式を F の線形代数的評価式と呼ぼう。 素式の F の評価式は (1) である。より複雑な論理式の 評価式を以下帰納的に定める。まず否定については [[¬F]] = 1 − [[F]] (2) により計算する。F を素式 r(ei, ej)とし、関係 r を表現 する行列 R について Rc_を Rc def= 1 − R により導入する。ここで1 は成分が全て 1 であるよう な N× N 行列である3。Rcは R が 1-0 行列 (各成分が 1, 0)の場合各成分の 1, 0 を反転させたものである。 3_eT i1ej= 1が成立する。

すると¬r(ei, ej)の評価式は [[¬r(ei, ej)]] = eTi(1 − R)ej= eTiRcej (3) となる。連言と選言については [[F1∧ ··· ∧ FK]] def = [[F1]]···[[FK]] (4) [[F1∨ ··· ∨ FK]] def = min1{[[F1]] +··· + [[FK]]} (5) により評価する。但し min1(·) は thresholding 関数で min1(x) = { 1 if x≥ 1 x それ以外 により定義される。以上により閉式 F が限量子を持た ない場合、(1),(2),(3), (4),(5) に従って線形空間で評価す ることにより M での真偽値 [[F]]∈ {1,0} 得ることがで きる。 次に F が限量子を含む場合の評価式を導こう。我々 は存在限量子∃ を命題の選言を表すものと見なし、全 称限量子∀ は ¬∃¬ に置き換えて扱う。例として論理式 ∃yr1(x, y)∧ r2(y, z)の評価を行おう。R1, R2を r1, r2を 表現する行列とする。∑N_j=1ejejT が単位行列になるこ とに注意すると [[∃yr1(x, y)∧ r2(y, z)]] = [[(r1(x, e1)∧ r2(e1, z))∨ ··· ∨ (r1(x, eN)∧ r2(eN, z))]] = min1 ( N

∑

j=1 [[r1(x, ej)∧ r2(ej, z)]] ) = min1 ( N

∑

j=1 xTR1ejejTR2z ) = xTmin1 ( R1 ( N

∑

j=1 ejejT ) R2 ) z = xTmin1(R1R2) z (6) を得る。min1(·) を行列に適用する場合、成分毎に適用 する。従って新しい２引数述語 rnew_{(x, z)とそれを表現} する行列 Rnew_を

rnew(x, z) def= ∃yr1(x, y)∧ r2(y, z) (7)

Rnew:2e def= min1(R1R2)

により導入すると rnew(x, z)の評価式

[[rnew(x, z)]] = (x• Rnewz) = xTRnewz

を得る。今の例は自由変数を含んでいたが、Horn 節を普 遍限量化された閉式と見た場合の評価式を∀x∀yr1(x, y)⇒

r2(x, y)について導こう。

[[∀x∀yr1(x, y)⇒ r2(x, y)]] = [[¬∃x∃yr1(x, y)∧ ¬r2(x, y)]]

= 1− min1 ( tr(R1Rc2 T₎) ₍₈₎ を得る。ここで tr(A) は行列 A のトレイスであり、tr(R1Rc2 T₎ は r1(x, y)⇒ r2(x, y)を満たさない (x, y)∈ D ×D の総数 である。∀x∀yr1(x, y)⇒ r2(x, y)が真⇔ tr(R1Rc2T) = 0 が分かる。 我々が提案する評価法が既存の論理式の連続値によ る評価法と異なる最大の点は、限量子の grounding 操作 は必須でなく、この例のように関係を matrix の操作だ けでも評価ができる可能性にある。これを同値式に応用 することにより、ある種のアルゴリズムの matrix によ る実装が得られる。例として、2 項関係 r1(x, y)の推移 閉包 (transitive closure)r2(x, y)の計算を考える。r1(x, y) と r2(x, y)については

r2(x, z)⇔ r1(x, z)∨ ∃y(r1(x, y)∧ r2(y, z)) for∀x,z ∈ D

が成立することより [[r2(x, z)]] = [[r1(x, z)∨ ∃y(r1(x, y)∧ r2(y, z))]]が得られる。R1, R2∈ {0,1}N×Nをそれぞれ関 係 r1(·,·),r2(·,·) を表す行列として評価式を導くと R2 に関する再帰的方定式 R2= min1(R1+ R1R2) を得る。この最小解が r1(x, y)の推移閉包行列であるが、 min1(·) の非線形性を回避しつつ、逆行列を使って R2 を高速に計算することができる。実際 N = 104と置き、 R1をランダムに生成して、その推移閉包を我々の方法 で計算してみると、Prolog 処理系や ASP 処理系に比較 して非常に高速に (10 倍から 104_{倍の速度で) 動作する} ことが分かった（詳細省略）。

4

限量子のテンソル表現と冠頭標準

形の線形代数的評価

前節では 2 項関係のみを扱ったが、この節では任意 の多項関係を扱い、また存在限量子のテンソル表現を 導入して、冠頭標準形を統語的に isomorphic な線形代 数的評価式に map する方法を（紙面の都合上）例に より解説する。まず解説に使うテンソル関連の記号を 導入する。テンソルは数学的に捉えるときは多重線形 写像として理解し、データ構造としては多次元配列と して扱う。テンソル A ={ai1,...,ip} と B = {bk1,...,kq} の

mode-(n,m) 縮約積 (contracted product) (A×n,mB)は、

成分表示で (A×n,mB)i1,...,in−1,in+1,...,ip,k1,...,km−1,km+1,...,kq=

∑jai1,...,in−1, j,...,ipbk1,...,km−1, j,...,kqにより定義される。縮約 積の結合は左優先で A×n,mB×p,qC = (A×n,mB)×p,qC

である。ベクトルの外積 (outer product) からテンソル が作られる。例えばベクトル a, b, c から order-3 のテン ソル (a◦ b ◦ c)i jk= aibjckが定義される。 さて一般の論理式 F の線形代数的評価を考える際、 真偽値は変わらないので F に同値な冠頭標準形の線形 代数的評価を考えれば良い。そのため冠頭標準形の線 形代数的評価式を導く。まず M の k 項関係 r を持つ ground atom r(ei1, . . . , eik)は成分が 0,1 であるようなテ ンソル R ={ri1,...,ik} を用いて

[[r(ei1, . . . , eik)]]

= R(ei1, . . . , eik) as multilinear map = R×1,1ei1×1,2··· ×1,ikeik = ri1,...,ik∈ {1,0} (∀i1, . . . , ik∈ {1,...,N}) (9) により評価される。ri1,...,ik は M に於ける r(ei1, . . . , eik) の真偽値であり、R を r を表現するテンソルと呼ぶ。 一方冠頭標準形の線形代数的評価は存在限量化され たリテラルの連言∃y(L1∧ ··· ∧ LM)の線形代数的評価 に帰着させることが出来る。 一般性を失うことなく変数 y はすべてのリテラル Lm (1≤ m ≤ M) に出現し、Lmの引数は y を含む相異なる 変数から成り、更に m̸= m′ならば Lmと Lm′は y を除 いて共通変数を持たない仮定する（そうでない場合は Mの適切な述語を導入し、仮定を満たすようにする）。 リテラル Lmの述語記号を rm、引数変数を並べた行ベ クトルを x(m)と記すと Lm= r◦m(x(m))と書ける。但し Lmが正リテラルなら r◦m= rmであり、負リテラルなら r◦_m=¬rmである。R◦mを rm◦を表現するテンソルとする。 x(m)から（順序を保存したまま）y を削除した行ベクト ルを x(m)_−y と記す。すると [[∃y(L1∧ ··· ∧ LM)]] = [[∃y(r₁◦(x(1))∧ ··· ∧ r◦_M(x(M)))]] = min1 ( N

∑

k=1 M

∏

m=1 R◦_m(x(m))_y←ek ) = min1 ( N

∑

k=1 M

∏

m=1 (R◦_m•jmek)(x(m)_−y) ) = min1 ( N

∑

k=1 {( (R◦₁•j1ek)◦ ··· ◦ (R ◦ M•jMek) ) (x(1)_−y, . . . , x(M)_−y) }) = min1 ( N

∑

k=1 ( ( M z }| { ek◦ ··· ◦ ek)×1, j1R ◦ 1×1, j2··· ×1, jMR ◦ M )) (x(1)_−y, . . . , x(M)_−y) = min1 ( Q∃,M×1, j1R ◦ 1×1, j2··· ×1, jMR ◦ M ) (x(1)_−y, . . . , x(M)_−y) where Q∃,M= N

∑

k=1 M z }| { ek◦ ··· ◦ ek. が得られる。ここで存在限量子∃ はテンソル Q∃,Mに より表現され、k =|x(1)_{| + ··· + |x}(M)_{| − M と置くと、} ∃y(L1∧ ··· ∧ LM)が定める M の k 項関係は (10) に定め る Rnewにより表現される。 Rnew= min1 ( Q∃,M×1, j1R ◦ 1×1, j2··· ×1, jMR ◦ M ) (10)

5

冠頭標準形の線形代数的評価例

(10)を利用して、新述語（新らしい関係）を導入し つつ、与えられた冠頭標準形 F を内側から簡単化する ことにより、F の線形代数的評価式系ΣFが得られる。 ΣFを順次評価することにより、F の真偽値が得られる。 簡単な評価例を示す。自由変数を持たない冠頭標準形 FABCD=∀x∃y((A(x,y)∧B(x))∨(C(x,y)∧D(y))、および M上の関係 A, B,C, D を表すテンソル A, B, C が与えら れているとする。FABCDの評価式系ΣFABCDを求める。以 下、存在限量化されたリテラルの連言∃y(L1∧···∧LM) の選言を∃-DNF と呼ぶ。 まずΣFABCD={} と置き、FABCDの最も内側の限量子 を持つ部分式を F2と置いて F2を∃-DNF に同値変形す る（FABCD=∀xF2である）：

F2 = ∃y((A(x,y) ∧ B(x)) ∨ (C(x,y) ∧ D(y)))

= ∃y(A(x,y) ∧ B(x)) ∨ ∃y(C(x,y) ∧ D(y)) = (∃yA(x,y) ∧ B(x)) ∨ ∃y(C(x,y) ∧ D(y)) 次に M 上の新しい関係 rnew_A , r_CDnewを導入して F2を開

式（束縛変数を持たない式）G∗₂に書き換える：

r_Anew(x) ⇔ ∃yA(x,y)

r_CDnew(x) ⇔ ∃y(C(x,y) ∧ D(y))

G∗₂ = (r_Anew(x)∧ B(x)) ∨ r_CDnew(x). 対応して、これらの新しい関係を表すテンソル Rnew_A , Rnew_CD を導入し、ΣFに加える： Rnew_A = min1(Q∃,1×1,2A) (11) Rnew_CD = min1(Q∃,2×1,2C×1,1D) (12) 以上の操作により FABCDの一番内側の限量化式 F2か ら∃y が除去された。以後 F2の一つ外側の限量化され た式 F1を F1=∀xF2=∀xG∗2と置いて評価式の導出を 続ける。F1を（∃-DNF とは双対の）∀-CNF に同値変形 する： F1 = ∀x((rAnew(x)∧ B(x)) ∨ rCDnew(x))

次に M 上の新しい関係 rnew

ACD, rnewBCDを導入して F1を開

式 G∗₁に書き換える：

r_ACDnew ⇔ ∀x(rnew_A (x)∧ rnew_CD(x))

rnew_BCD ⇔ ∀x(rB(x)∧ rCDnew(x))

G∗₁ = r_ACDnew ∧ r_BCDnew

それから、rnew

ACD, rnewBCDを表すテンソル (scalar) を導入し、

ΣFABCDに加える：

Rnew_ACD = 1− min1(Q∃,2×1,1¬RnewA ×1,1¬RCDnew)(13)

Rnew_BCD = 1− min1(Q∃,2×1,1¬B ×1,1¬RnewCD) (14)

ΣFABCD={(11),(12),(13),(14)} である。

以上の操作で FABCDの限量子は全て除去され、ΣFABCD

に蓄えられた新述語により FABCDは命題論理式 F0に書

き換えられる：

F0 = G∗1 = rnewACD∧ rnewBCD

Mに於ける FABCDの真偽値 [[FABCD]]は [[F0]]に等し

く、F0の評価式：

[[F0]] = RnewACD· RnewBCD

をΣFABCD={(11),(12),(13),(14)} を用いて評価するこ とにより [[FABCD]]が得られる。付録に冠頭標準形の一 般的線形代数的評価アルゴリズムが記載してある。

6

おわりに

述語論理の各種推論は古典的 AI の根幹であったが、 最近の KG（知識グラフ）の出現とともに、個体を実ベ クトルに、関係を行列に変換して、線形代数的実数計 算を使って論理的推論を行う試みが盛んになっている。 本論文の貢献は２つある。 • 限量子をテンソル化し、限量化された一階述語 論理式の評価をテンソルを使って線形代数的に行 う方式を提案した。言い換えると初めて Tarskian semanticsを線形空間に埋め込んだ。Grefenstette のテンソル化の研究 [4] では開式と限量化された 式は別々に取り扱われ、統一された意味論的枠組 みになっていない。また、Rocktaschel などのア プローチ [10, 11, 6, 13] では限量子自体の表現は なく、限量子は grounding して命題論式に還元さ れた式を線形代数的に扱っているだけである。 我々は限量子にテンソル表現を与えると同時に、 一つの枠組みで Tarskian semantics を線形空間に 埋め込んでいる。その結果、ここでは述べなかっ たが従来のアプローチの問題点とともに Tarskian semanticsの低次元埋め込みに於ける限量子の役 割が明確となった。 • 論理等式からテンソル（行列）の再帰的線形代数 的方程式を導くことにより、再帰的アルゴリズム を効率よく実装できる可能性を示した。実際実験 も行っており、この方式の有望さを確認している。 また本方式は現代的非単調論理で中心的役割を果 たす stable model （安定化モデル）の計算にも応 用可能であり、ASP（解集合プログラミング）の 記号的評価法とは異なる scalable な評価法の実現 が期待される。 最初にも述べたとおり、本論文は論理の線形代数的 計算の世界を探る上で、最も基本的な部分、Tarskian semanticsの線形空間への埋め込みを扱ったに過ぎな い。発想推論や帰納推論の線形代数的形式化、あるい は低次元線形空間の埋め込みによる近似的論理計算な ど探求すべき未知の部分は多く、また自然言語処理へ の応用など成すべき課題は山積している。

参考文献

[1] Kurt Bollacker, Colin Evans, Praveen Paritosh, Tim Sturge, and Jamie Taylor. Freebase: a collabora-tively created graph database for structuring human knowledge. In Proceedings of the 2008 ACM

SIG-MOD International Conference on Management of data, pages 1247–1250, 2008.

[2] Xin Dong, Evgeniy Gabrilovich, Geremy Heitz, Wilko Horn, Ni Lao, Kevin Murphy, Thomas Strohmann, Shaohua Sun, and Wei Zhang. Knowl-edge Vault: A Web-Scale Approach to Probabilis-tic Knowledge Fusion. In Proceedings of the 20th

ACM SIGKDD International Conference on Knowl-edge Discovery and Data Mining, KDD2014, pages

601–610, 2014.

[3] Luis Antonio Gal´arraga, Christina Teflioudi, Katja Hose, and Fabian Suchanek. Amie: Association rule mining under incomplete evidence in ontologi-cal knowledge bases. In Proceedings of the 22Nd

In-ternational Conference on World Wide Web, WWW

’13, pages 413–422, New York, NY, USA, 2013. ACM.

[4] Edward Grefenstette. Towards a Formal Distribu-tional Semantics: Simulating Logical Calculi with Tensors. Proceedings of the Second Joint

Confer-ence on Lexical and Computational Semantics, pages

[5] Kelvin Guu, John Miller, and Percy Liang. Travers-ing Knowledge Graphs in Vector Space. In

Proceed-ings of the 2015 Empirical Methods in Natural Lan-guage Processing (EMNLP), pages 318–327, 2015.

[6] Denis Krompaß, Maximilian Nickel, and Volker Tresp. Querying Factorized Probabilistic Triple Databases. In Proceedings of the 13th

Interna-tional Semantic Web Conference(ISWC’14), pages

114–129, 2014.

[7] Maximilian Nickel. Tensor factorization for rela-tional learning. In PhD Thesis,

Ludwig-Maximilians-Universitat Munchen, 2013.

[8] Maximilian Nickel, Kevin Murphy, Volker Tresp, and Evgeniy Gabrilovich. A Review of Rela-tional Machine Learning for Knowledge Graphs: From Multi-Relational Link Prediction to Auto-mated Knowledge Graph Construction. CoRR,

abs/1503.00759, 2015.

[9] Maximilian Nickel, Volker Tresp, and Hans-Peter Kriegel. A Three-Way Model for Collective Learn-ing on Multi-Relational Data. In ProceedLearn-ings of the

28th International Conference on Machine Learning,

2011.

[10] Tim Rockt¨aschel, Matko Bosnjak, Sameer Singh, and Sebastian Riedel. Low-Dimensional Embed-dings of Logic. In ACL Workshop on Semantic

Pars-ing (SP’14), 2014.

[11] Tim Rockt¨aschel, Sameer Singh, and Sebastian Riedel. Injecting Logical Background Knowledge into Embeddings for Relation Extraction. In Annual

Conference of the North American Chapter of the Association for Computational Linguistics (NAACL),

2015.

[12] Fabian M. Suchanek, Gjergji Kasneci, and Gerhard Weikum. YAGO: A Core of Semantic Knowledge Unifying WordNet and Wikipedia. In Proceedings

of the 16th International World Wide Web Confer-ence(WWW’07), pages 697–706, 2007.

[13] Bishan Yang, Wen-tau Yih, Xiaodong He, Jianfeng Gao, and Li Deng. Embedding Entities and Relations for Learning and Inference in Knowledge Bases. In Proceedings of the International Conference on

Learning Representations (ICLR) 2015, 2015.

A

付録

Input: A model M for a first-order language L with finitely many constants and a first-order closed for-mula F = Q1x1···QmxmG inL in prenex normal

form such that no atom has duplicate variables and G is an open DNF or CNF

Procedure:

[Step 1] SetΣF={}, Gm= G and Fm= QmxmGm;

[Step 2]

Fori = m down-to 1 Do Write Fi= QixiGi;

If Qi=∀ then goto [Step 2-B];

[Step 2-A]

Convert QixiGito∃-DNF G∗i;

For eachdisjunct D in G∗_i Do

Write D =∃y(L1∧ ··· ∧ LM)∧ D′where y occurs

once

in each Li (1≤ i ≤ M) and has no occurrence

in D′;

Let xfreebe an enumeration without duplication of

free variables in D′′=∃y(L1∧ ··· ∧ LM);

Define a new atom by rnew(xfree)⇔ D′′;

Replace D in G∗_i with rnew(xfree)∧ D′;

Introduce a new tensor Rnewby (10) encoding the new relation rnew_{in M;}

Add toΣFthe tensor definition for Rnew;

endDo

Set F_i−1= Q_i−1x_i−1G∗_i; [Step 2-B]

Convert QixiGito∀-CNF Ci∗;

(the rest is dual to [Step 2-A] and omitted) endDo

[Step 3] If F0= r1∧ ··· ∧ rhthen put Ftensor= r1···rh;

Else F0= r1∨ ··· ∨ rhand put Ftensor= min1(r1+

··· + rh);

(ri’s are atoms with no arguments, equated with

true or false, and hence with{1,0})

Output: Ftensor with a set ΣF of tensor definitions. ΣF

ΣFencodes new M-relations appearing in S and F0

gives [[F]] in M.