日本ソフトウェア科学会第 34 回大会 (2017 年度) 講演論文集

極大完備化に基づく等式定理の自動証明
萩原 崇央

青戸 等人

項書き換えシステムの代表的な自動証明法として，クヌース・ベンディクス完備化がある．失敗無し完備化 (Bachmairら，1989) はクヌース・ベンディクス完備化を利用した等式の定理自動証明法である．一方，完備化の新しい手法として，極大完備化 (Klein&広川，2011) が提案されている．極大完備化は，パラメータとして簡約順序を必要としな
い，SMT ソルバを活用した完備化手法である．本報告では，極大完備化を失敗無し極大完備化へと拡張する．具体的には，等式判定手続きへの変更，変数のスコーレム定数への置き換え，向き付け不能な等式による書き換え手続きの追加，柔軟な危険対生成手続きの導入を行い，極大完備化に基づく等式定理の自動証明システムを実現した．また，実装したシステムによる定理証明実験の結果を報告する．

標に完備化手続きを走らせる，失敗無し完備化 [1] が

1 はじめに知られている．失敗無し完備化は，完備化自体が失敗等式論理の定理自動証明法として，項書き換えシスする場合であっても，等式定理証明に成功する場合もテム (TRS) による完備化は代表的なものである．完あることが知られており，実際には重要な定理証明法

備な TRS とは，停止性と合流性をもった TRS のこである．しかしながら，極大完備化に基づく失敗無しとであり，完備化とは，与えられた等式集合から，等完備化はまだ実現されていない．

価で完備な TRS を構成することである．等価で完備

本報告では，極大完備化に基づく失敗無し完備化をな TRS を用いると，等式定理の判定を行うことがで考案し，KB 完備化の代わりに極大完備化を用いて等きる．

式定理の自動証明法を実現する．具体的には，等式判完備化の代表的な手法として，クヌース・ベンディ

定手続きへの変更，変数のスコーレム定数への置き換

クス (KB) 完備化 [4] が知られている．KB 完備化はえ，向き付け不能な等式による書き換え手続きの追パラメータとして簡約化順序を用いるが，KB 完備化

加，柔軟な危険対生成手続きの導入を行い，極大完備が成功するかどうかは，用いる簡約順序に依存する．

化に基づく等式定理の自動証明システムを実現した．

Klein と広川 [3] によって提案された極大完備化は，また，実装したシステムによる定理証明実験の結果を改良の著しい SMT ソルバを活用した完備化手法であ報告する．

り，KB 完備化と遜色ない強力さを持つことが実験的にも確認されている．極大完備化では，最終的な完備

2 準備な TRS を発見するまで，簡約順序を固定しないまま2. 1 項書き換えシステム動作する．

本報告で用いる定義や記法について説明する．

KB 完備化においては，与えられた等式の証明を目関数の集合を F で表し，変数の集合を V で表す．

Automated Equational Theorem Proving based on
Maximal Completion
Takahisa Hagihara,Takahito Aoto, 新潟大学大学院自然科学研究科, Graduate School of Science and Technology, Niigata University.

V (t) は項 t 中の変数の集合を表す．項の全体集合をT (F, V ) で表す．|t| は項 t のサイズを表す．tσ は項t に対して代入 σ を適用して得られた項を表す．
文脈とは，特別な定数 2(ホール) をただ一つ含む

Deduce :⟨E, R⟩⟨E ∪ {s ≈ t}, R⟩

Delete :⟨E ∪ {s ≈ s}, R⟩⟨E, R⟩

Compose :⟨E, R ∪ {s → t}⟩⟨E, R ∪ {s → u}⟩s ←R u →R tt →R u
図1

Orient :˙ t}, R⟩⟨E ∪ {s ≈⟨E, R ∪ {s → t}⟩s≻t

Simplify :˙ t}, R⟩⟨E ∪ {s ≈⟨E ∪ {u ≈ t}, R⟩

s →R uCollapse :⟨E, R ∪ {s → t}⟩⟨E ∪ {u ≈ t}, R⟩

s →R,l→r u

KB 完備化の推論規則項のことをいう．ホールの位置が p であるような文脈

し，l1 → r1 = l2 → r2 のとき，p は根位置でないもC を C[ ]p と記す．t[]p は項 t の位置 p をホールに置のとする．
∗∗

き換えて得られる文脈を表す．C[t] は文脈 C のホー

任意の項 s, t, u について，s ←−R u −→R t ならば，ルを項 t で置き換えて得られる項を表す．t|p は項 tある項 w が存在して，s −→R w ←−R t となるとき，項の位置 p の部分項を表す．t  s は ∃σ.t|p = sσ かつ

書き換えシステム R は合流性を持つという．項書きt ̸= s を表す．

換えシステム R が停止性と合流性を持つとき，項書2 つの項 l, r が l ̸∈ V, V (r) ⊆ V (l) を満たすとき，∗∗

き換えシステム R は完備であるという．

l → r を書き換え規則とよぶ．さらに，書き換え規˙ t
項の等式 s ≈ t と t ≈ s を同一視するときは s ≈則の集合を項書き換えシステム (TRS) という．R を˙ t ∈ E ，代入と記す．E を等式集合とする．等式 s ≈項書き換えシステムとする．書き換え規則 l → r ∈σ ，文脈 C[]p が存在して，s = C[lσ]p かつ t = C[rσ]pR，代入 σ ，文脈 C[ ]p が存在して，s = C[lσ]p かつとなるとき，s ↔E t と記す．等式 s ≈ t が等式集合

t = C[rσ]p となるとき，s →R t と記す．s →R t にE の定理であるとは，s ↔E t となることをいう．

∗∗

おいて，用いた書き換え規則 l → r ∈ R を明示する∗

場合には，s →R,l→r t と記す．s →R t は →R の反∗射推移閉包を，↔R は →R の等価閉包を表す．

2. 2 クヌース・ベンディクス完備化
完備化の標準的な手法であるクヌース・ベンディ

項書き換えシステム R に対して，項 s が正規形であクス (KB) 完備化手続き [1] [4] を定義する．KB 完るとは， s →R t となるような t が存在しないときを備化では図 1 の推論規則を用いて完備化を行う．図

∗いう．正規形の集合を NF と記す．s →R t ∈ N F と1 の推論規則による導出を ⊢ と表す．⊢∗ と表記しなるとき，項 t を項 s の正規形とよび，s↓R で表わす．

た場合，0 回以上の導出を表す．⟨E, ∅⟩ = ⟨E0 , R0 ⟩また，項の集合 T について，T ↓R = {s↓R | s ∈ T }⊢∗ ⟨En , Rn ⟩ = ⟨∅, R⟩ なる導出が公平であるとは，∩∃i.⟨s, t⟩ ∈CP (Rj ) ならば，∃k.s ≈ t ∈ Ek であと定義する．

i≤j

無限書き換え列 t0 →R t1 →R · · · が存在しないとることをいう．KB 完備化手続きとは，等式集合 E ，き，項書き換えシステム R は停止性を持つといい，簡約順序 ≻ を入力とし，⟨E, ∅⟩ ⊢∗ ⟨∅, R⟩ となる公平

SN (R) と記す．代入及び文脈に閉じている整礎な項な導出を構成する手続きをいう [4]．

上の半順序を簡約順序という．

命題 2.1 (KB 完備化手続きの正しさ) 等式集合 E ，R を項書き換えシステム，l1 → r1 ∈ R, l2 → r2 ∈簡約順序 ≻ を KB 完備化手続きの入力とする．このR を書き換え規則とする (一般性を失うことなく，共とき，項書き換えシステム R が出力されるならば，R通変数を持たないものとする)．l2 のある非変数部分項は完備かつ ↔E = ↔R となる．

∗∗

l2 |p と l1 が単一化可能であるとき，位置 p で l1 → r1

KB 完備化は簡約順序を固定して完備化を行うたが l2 → r2 へ重なるという．代入 σ を l2 |p と l1 の最め，手続きの成功や効率は，用いる簡約順序に大きく汎単一化子とするとき，項の対 ⟨l2 [r1 ]p σ, r2 σ⟩ を危険依存する．

対とよび，R の危険対の集合を CP (R) で表す．ただDeduce2 :⟨E, R⟩⟨E ∪ {s ≈ t}, R⟩s ↔E∪R u ↔E∪R t ∧ s ̸≻ u ∧ t ̸≻ u

Simplify2 :˙ t}, R⟩⟨E ∪ {s ≈⟨E ∪ {u ≈ t}, R⟩

s →E≻ ,lσ→rσ u ∧ s  lCompose2 :⟨E, R ∪ {s → t}⟩⟨E, R ∪ {s → u}⟩t →E≻ uCollapse2 :⟨E, R ∪ {s → t}⟩⟨E ∪ {u ≈ t}, R⟩

s →E≻ ,lσ→rσ v ∧ s  l

図2

失敗無し完備化の推論規則

2. 3 失敗無し完備化

合 E ，等式 s ≈ t，完全な簡約順序 ≻ を失敗無し

失敗無し完備化 [1] は KB 完備化を等式定理証明に完備化手続きの入力とする．失敗無し完備化手続きが成功するとき，等式 s ≈ t は E の定理である．

拡張した手続きである．
失敗無し完備化は KB 完備化に図 2 の推論規則を追加する．ここで，E≻ は E≻ = {lσ → rσ | l ≈ r ∈3 極大完備化に基づく等式定理証明

E, lσ ≻ rσ} と定義される項書き換えシステムであ3. 1 極大完備化

る．また，Deduce2 は Deduce の拡張となっている

極大完備化は Klein と広川 [3] によって提案されたことに注意する．失敗無し完備化では，危険対の代完備化手法である．極大完備化では，入力として等式わりに拡張危険対 [1] を用いる．項書き換えシステム

集合 E だけを与え，↔R = ↔E かつ完備な項書き換

R，等式集合 E とし，σ を最汎単一化子，書き換ええシステム R を発見する．極大完備化手続きを以下

˙ r1 ∈ E は，位置 p
規則 l1 → r1 ∈ R もしくは l1 ≈で与える．

∗∗˙ r2 ∈ E へ重なるとすで l2 → r2 ∈ R もしくは l2 ≈入力： 等式集合 Eる．このとき，r2 σ ̸≻ l2 σ で r1 σ ̸≻ l1 σ となる等式

出力： 完備かつ ↔E = ↔R な項書き換えシスr2 σ ≈ l2 σ[r1 σ]p を拡張危険対と呼ぶ．等式集合 E ∪R∗∗

テム Rの間の全ての拡張危険対の集合を ECP≻ (E ∪ R) とStep 1 C := E表す．

Step 2 R1 , ..., Rk ∈ max T (C) を見つける．

以 下 で は ，項 t 中 の 変 数 全 て を 定 数

Step 3 それぞれの 1 ≤ i ≤ k について，化 (ス コ ー レ ム 化) し た 項 を t̂ と 表 す．ま(3-1) NF i := (CP (Ri ) ∪ E)↓Ri

た ，eq, True, False を 新 し い 関 数 記 号 と す(3-2) NF i = ∅ なら完備化に成功し，R := Riる ．⟨E ∪ {eq(x, x) ≈ True, eq(ŝ, t̂) ≈ False}, ∅⟩を出力して終了．

=∗⟨E0 , R0 ⟩ ⊢ ⟨En , Rn ⟩ = ⟨∅, R⟩ なる導出が公平で∩あるとは，∃i. ⟨s, t⟩ ∈ECP ≻ (Rj ) ならば，∃k. s ≈(3-3) NF i ̸= ∅ なら Ci := N Fi \ Id∪Step 4 C := C ∪Ci とし，Step 2 へ戻る．

i≤j1≤i≤kt ∈ Ek であることをいう．失敗無し完備化手続きとは，等式集合 E ，等式 s ≈ t，完全な簡約順序 ≻ を入

ここで，力とし， ⟨E, ∪{eq(x, x) ≈ True, eq(ŝ, t̂) ≈ False}, ∅⟩Id = {u ≈ u | u ∈ T (F, V )}= ⟨E0 .R0 ⟩ ⊢∗ ⟨En , Rn ⟩,True ≈ False ∈ Ei なる公平

T (C) = {R | R ⊆ C ∪ C −1 , SN (R)}な導出を構成する手続きをいう．
失敗無し完備化手続きの正しさは文献 [1] に与えら

max{R1 , . . . , Rn } = {Ri | ¬∃Rj . Ri ⊊ Rj }極大完備化手続きの正しさは文献 [3] で与えられてれている．

いる．

命題 2.2 (失敗無し完備化手続きの正しさ) 等 式 集命題 3.1 (極大完備化手続きの正しさ) 等 式 集 合 E

を極大完備化手続きの入力とする．項書き換えシステ∗∗

ム R が出力されるならば，R は完備かつ ↔E = ↔R

4 失敗無し極大完備化の実装となる．

4. 1 極大完備化のヒューリスティックス
極大完備化手続きは素朴に実装すると，等式集合 C

3. 2 失敗無し極大完備化がとても大きくなるため，計算時間が増え，成功に至

この節では極大完備化を等式定理証明に拡張する．

らない場合が多い．そこで，極大完備化では，Step 2失敗無し極大完備化手続きを以下に示す．

で発見する項書き換えシステムの個数 k に上限を設

入力： 等式集合 E ，等式 s ≈ t

ける．さらに，Step 4 で C に追加する等式の制限を出力： 成功行うことで，効率の良い完備化手続きを実現する [3]．

Step 1 C := E ∪ {eq(x, x) ≈ True, eq(ŝ, t̂) ≈定義 4.1 (k の上限 [3]) K の 初 期 値 を 1 と す る ．

Step 2 で K を用いるように変更し，k ≤ K とすFalse}
Step 2 (R1 , ≻1 ), . . . , (Rk , ≻k ) ∈ max T (C) を見つける．

Step 3 それぞれの 1 ≤ i ≤ k について
(3-1) NF 1i := (ECP ≻i (C ∪ Ri ) ∪ E)↓Ri(3-2) NF 2i := {(u′ ≈ v | u →C≻i ,lσ→rσ′

˙ v ∈ C}u , u  l, u ≈˙ False ∈ NF1 i ∪ NF2 i なら証明
(3-3) True ≈る．Step 4 で K を以下の様に変更する．
∪ K +1 (Ci ⊆ C のとき)
1≤i≤kK= K(その他の場合)
定義 4.2 (C のフィルタリング [3]) 項の大きさに関する C のフィルタリング C <d を以下のように定義する．

C <d = {s ≈ t ∈ C | |s| + |t| < d}成功．

˙ False ̸∈ NF1 i ∪ NF2 i な ら(3-4) True ≈さらに，C の中からサイズの小さい順に n 個抜き出

Ci := (NF1 i ∪ NF2 i ) \ Id∪
Step 4 C := C ∪Ci とし，Step 2 へ戻る．

したものを C↑n と記す．これらのパラメータを用い

1≤i≤kて Step 4 を以下の様に変更する．
∪ <dC := C ∪ (Ci )↑n1≤i≤k

ここで，(Ri , ≻i ) ∈ max T (C) は，Ri ∈ max T (C)

我々の実装でも，これらのパラメータは Klein と広かつ ≻i が Ri ⊆ ≻i なる簡約順序であることを表す．

川の実装 [3] に従い，n = 7，d = 20 の値を用いる．

極大完備化手続きとの差分は以下の通りである．

• Step 1 の C の 初 期 値 を C := E か ら C :=E ∪ {eq(x, x) ≈ True, eq(ŝ, t̂) ≈ False} に変更．
• Step 3 における危険対を拡張危険対に変更．
• Simplify2 ，Compose2 ，Collapse2 の規則追加のための手続き (3-2) を追加．

˙ False ∈ NF 1i ∪ NF 2i• 手続きの終了条件を True ≈かどうかに変更．
以下の定理を容易に示すことが出来る．

4. 2 失敗無し極大完備化のヒューリスティック (1)極大完備化では，d は定数であったが，失敗無し極大完備化では
d を以下の様に変更する．
 20(m ≤ 20 のとき)d=
 m + 8 (その他の場合)
ここで，m = max{|s| + |t| | s ≈ t ∈ E} とする．
これは，|s| + |t| > 20 となる等式を含む E に対応す∪
Ci ⊆ C が 3 回連続るためである．Step 4 で，
1≤i≤k定理 3.2 (失敗無し極大完備化手続きの正しさ) 等式

した場合，d と K の値を以下の様に変更する．

集合 E ，等式 s ≈ t を失敗無し極大完備化手続きの• d := d + 2入力とする．このとき，手続きが成功するならば，等• K := K − 3式 s ≈ t は E の定理である．

これは，手続きの途中で d 以上の等式しか生成されない可能性に対応するためである．

4. 3 失敗無し極大完備化のヒューリスティック (2)成功した例は COL003-12，COL003-13，REL49-1，

失敗無し極大完備化ではさらに，Step 4 で追加さRNG008-4 の 4 例である．

れなかった等式を保存するリストを導入した．これは，小さい等式から C へ追加する機能を強化するた

6 まとめと今後の課題めである．失敗無し極大完備化手続きの Step 4 を以極大完備化を失敗無し完備化に拡張した等式定理証明法である失敗無し極大完備化を提案した．最近

下に変更する．

Step 4∪

P := P ∪ (同様な極大完備化を基にした等式定理証明システムC)<dmaedmax が提案されているが，maedmax で用いら

1≤i≤kC := C ∪ (P ↑n )

れている手法との比較や，より強力な極大完備化にP := (P \ (P ↑n ))↑m

基づく等式定理証明法は今後の課題の検討課題であ

ただし，m = 75 を用いる．

る．我々の手法を実装した unfMax は maedmax に比べて成功数が少なかったが，maedmax では成功し5 実験結果と考察なかった例について，unfMax は成功した．

提案手法に基づく定理自動証明システム unfMax

今後の課題としては，maedmax では定理証明に成を実装した．unfMax は関数型言語 SML を用いて実功し unfMax では失敗した問題や，unfMax で定理装しており，プログラムの行数は約 2500 行である．

証明に成功し，maedmax では失敗した問題について

また，手続き内で SMT ソルバである Yices1.0 [2] をその要因を探る必要がある．また，より効率の良い用いた．

ヒューリスティクスを発見することにより，証明成功実験には，定理証明の問題集である TPTP 6.4.0率の向上を図ることが挙げられる．

[6]Unit Equality Problem(UEQ) を用いた．極大完備化を基にした定理自動証明システムである maedmax

参 考 文 献[7] および，多重 KB 完備化を基にした定理自動証明[1] Bachmair, L., Dershowitz, N., and Plaisted,
D. A.: Completion without failure, Resolution ofEquations in Algebraic Structures, Vol. 2, Academic
Press Inc., 1989.
[2] Dutertre, R. and de Moura, L.: The Yices SMT
Solver. http://yices.csl.sri.com/.
[3] Klein, D. and Hirokawa, N.: Maximal completion,
Proc. of 22nd RTA, LIPIcs, Vol. 10, 2011, pp. 71–80.
[4] Knuth, D. E. and Bendix, P.: Simple word problems in universal algebras, Computational Problems
in Abstract Algebra, Leech, J.(ed.), Pergamon Press,
1970, pp. 263–297.
[5] Sato, H., Winkler, S., Kurihara, M., and Middeldorp, A.: Multi-completion with termination tools(system description), Proc. of 4th IJCAR, LNAI,
Vol. 5195, 2008, pp. 306–312.
[6] Sutcliﬀe, G. and Suttner, C.: The TPTP Problem Library for Automated Theorem Proving. http://www.cs.miami.edu/~tptp/.
[7] Winkler, S.: Maximal Ordered Completion. http://cl-informatik.uibk.ac.at/software/maedmax/.

システムである mkbTT [5] と比較した．表 1 に実験結果を示す．unfMax は timeout を 7 分とし，CPU：AMD phenomII x6 2.80GHz，RAM：16GB の PC
上で実験結果である．maedmax，mkbTT の実験結果はウェブページ [7] の引用である．

表1

等式定理証明の実験結果
unfMaxmaedmax

mkbTT

success

340

522

223

timeout

675

504762error

261556

成功個数は mkbTT < unfMax < maedmax となった．maedmax では定理証明に失敗し，unfMax では