ゲーム Hex における必勝手順の 構成法に関する研究
三島 健
電気通信大学大学院電気通信学研究科 博士（工学）の学位申請論文
2010 年 3 月
ゲーム Hex における必勝手順の 構成法に関する研究
博士論文審査委員会
主査 岩田 茂樹 教授 委員 中山 泰一 准教授 委員 笠井 琢美 教授 委員 小林 聡 教授
委員 野下 浩平 名誉教授
著作権保持者
三島 健
2010 年 3 月
ゲーム Hex における必勝手順の構成法に関する 研究
三島 健 概要
本論文では，ゲームHexにおける必勝手順の構成法に関する研究について述べる．
ゲームHexはP. Hein（1942年）やJ.F. Nash（1948年）によって考案された．1949年 に，J.F. Nashは，n×nの盤面において，先手が任意の初手を選べるとき，先手必勝で あることを証明した．C. Bergeは，盤面の解析における基本的な考え方である先行排 除の方法を提案した（1977年）．任意の盤面において勝利プレイヤを決定する問題は
PSPACE完全であることが証明されている（1981年）．2000年代になって，J. Yang
らやR. Haywardらによって，7×7における必勝手順が求められている．世界初の対
局プログラムは，C. Shannonらによって作成された（1953年）．C. Shannonらの着手 の評価法は，近年のQueen-bee（1999年）やHEXY（2002年）に応用されている．こ のように，今日まで多くの研究者達がHexにおける様々な研究課題に取り組んできた．
ゲームHexにおいて，具体的な必勝手順（構成的証明）を示すことは長年の研究課 題である．H.J. van den Herikら（2002年）は，“fundamental breakthrough”なしで は，8×8以上の必勝手順を扱えないと述べている．V.V. Anshelevich（2002年）は仮 想連結の概念を導入した．7×7では，J. Yangらが，decomposition methodと呼ばれ る盤面分割の方法を用いて，初手44（2001年）と初手53（2002年）における必勝手 順を求めた．R. Haywardら（2005年）が，コンピュータを用いることで，7×7 のす べての初手における勝利プレイヤを示した．K. Noshita（2005年）はユニオン連結や
AB-propertyの技法を提案し，これに基づき，8×8の必勝手順を簡潔な形で示した．
R. Haywardら（2006年）は，J. Yangの7×7の必勝手順の正しさを検証した．現在 では，8×8以上における具体的な必勝手順を示すことが可能になりつつある．今後，
より大きい盤面における必勝手順を導いていくために，効率的に必勝手順を導くため の証明法の開発が不可欠になっている．また，人間が盤面分割を行い，コンピュータ で検証を行うなどの共同作業が重要になってきている．
本論文の研究では，次の2つの成果を得た．第一に，必勝手順を効率的に導く新証 明技法として，σ連結の概念とσ拡張の技法を提案する．これらを用いることで，従来 の方法では必勝手順を求めることが複雑とされてきた8×8以上の大きな盤面に対し，
簡潔な形で必勝手順を構成できるようになった．第二に，盤面の連結性を検証するプ ログラムを提示する．性能評価実験を行った結果，8×8以上の必勝手順の検証・発見
のために，十分実用的な性能を持っていることがわかった．
第1章で，ゲームHexのルールを説明し，その研究背景について述べる．また，本 研究での新たな結果（第3章と第4章の内容）について，その概要を説明する．
第2章で，既存研究で示されている基本的な概念について述べ，本論文で用いる用 語や表記について説明する．
第3章で，石の連結性を表現するための新しい概念として，σ連結を定義し，それに 基づくσ拡張の技法を導入する．第3章の目的は，σ連結とσ拡張によって，新しい必 勝の証明法を確立し，必勝手順の構成に応用することである．まず，領域上での連結 の論理和と論理積を扱えるようにAND-OR連結を定義する．σ連結は，後手の着手に 対する先手の応手が指定されたAND-OR連結である．σ拡張は，σ連結の着手指定に 基づき，AND-OR連結に関与する領域を拡張する技法である．σ連結とσ拡張の応用 の例として，8×8（初手54）の先手必勝手順を従来の方法より簡単な形で示す．この 必勝手順を表す証明木の総節点数は13個である．
第4章で，与えられた局面に対してユニオン連結性を判定するプログラムを提示す る．本論文のプログラムは局面表を用いたAND-OR探索に基づくものである．仮想連 結や仮想準連結といったHex特有の概念を着手選択アルゴリズムに組み込むことで強 化した．性能評価実験を実施し，実行時間と探索節点について評価した．ベンチマー ク問題として，K. Noshitaによる7×7と8×8の必勝手順に現れる約40種類の難しい 問題を選んだ．実験結果によると，これらの局面の正しさを短時間で検証できた．プ ログラム上の着手選択（順序付けと先行排除）は，人間の熟練者と同程度に正確であ ると評価できる．本論文のプログラムは，8×8以上の必勝手順の検証・発見のために，
基本的な道具として使えることが明らかになった．
第5章で，本論文全体の総括を行う．
Studies on Construction Methods for Winning Strategies in Hex
Ken Mishima
ABSTRACT
In this thesis, we describe our studies related to methods for constructing winning strategies in the game of Hex. The rules of Hex was first designed by P. Hein (1942) and J.F. Nash (1948). J.F. Nash has proved that there exists a winning first-player strategy for any n× n board (1949). C. Berge (1977) has presented an important method to preclude trivial moves for a given position, which is often called must-play.
Determining a winning player for arbitrary positions has been proved to be PSPACE- complete (1981). In the 2000s, various winning strategies for 7×7 have been found (J. Yang et al. (2001, 2002), R. Hayward et al. (2005)). C. Shannonet al.(1953) have invented the first automated player. Their idea of the move evaluation has been used by recent computer players, such as Queen-bee (1999) and HEXY (2002). Thus many researchers have studied various research problems related to Hex for a long time.
In the game of Hex, constructing a winning strategy has been a long-standing re- search problem. H.J. Herik et al. (2002) stated that it has been regarded as complex to deal with a winning strategy for 8×8 or more without fundamental breakthrough.
V.V. Anshelevich (2002) introduced a notion of virtual connection. For 7×7, J. Yang et al. have shown two winning first-player strategies (first moves at 44 (2001) and 53 (2002)) based on their decomposition method. R. Hayward et al. (2005) have shown, for any opening move on the 7×7 board, a winning player has been determined by their computer program. K. Noshita (2005) constructed a complete winning strategy for 8×8 based on union-connection as well as AB-property. R. Hayward et al. (2006) has verified the correctness of Yang’s 7×7 winning strategy. Recently, it has been expected that winning strategies for 8×8 or more can be constructed. If we try to construct winning strategies on larger board sizes, it is indispensable to invent efficient proof methods for obtaining winning ways and to implement a system which enables human-computer cooperation based on them.
In this thesis, we describe two contributions of our studies. First, we present a notion of σ-connection and introduce a technique ofσ-extension for establishing a new method to show a winning way. The extensive use of our techniques enable us to
construct easy-to-verify winning strategies for relatively large boards of 8×8 or more.
Second, we present programs which verify the correctness of the connectivity for a given position. Our computing experiment shows that our programs can be of a practical use to verify/find winning strategies for 8×8 or more.
In chapter 1, we describe the research background including the rules of the game.
We also describe the outlines of our studies (chapter 3 and 4).
In chapter 2, we describe basic results known so far in the previous studies and our notations which will be used throughout this thesis.
In chapter 3, we present a new notion named σ-connection which defines a certain type of connections between stones. Based on it, we introduce a new technique named σ-extension. The purpose of this chapter is to establish a new method for proving the player’s win and applying it to construct a winning strategy. We define AND-OR connection for accommodating OR(union)-connections as well as AND-connections. A σ-connection is an AND-OR connection along with fixed move-sequences. Based on the fixed move-sequences, we can extend the area of empty cells which supports the desired AND-OR connection. This technique will be called σ-extension. Thanks to our σ-connection as well as σ-extension, it is possible to construct an easy-to-verify winning strategy for 8×8 with the first move at 54. This winning strategy as a proof tree consists of 13 nodes, 7 of which represent the positions of the second player’s turn.
In chapter 4, we present programs for testing whether, for a given position, a desired union-connection can be attained. Our programs are based on AND-OR searching with a transposition table, which is enhanced by Hex-dependent move-selection algorithms, such as virtual connections and virtual semi-connections. We evaluate the efficiency of those programs in terms of the running times as well as the number of searched nodes. For the set of benchmark problems, we have selected about forty hard positions from K. Noshita’s winning strategies for 7×7 and 8×8. Our computing experiment shows that the correctness of those positions has been verified very quickly in that our programs can be used for practical purposes. The quality of the move-selection (ordering and preclusion) can be evaluated to be as accurate as human expert players.
Our results show that our programs can be used as the most basic tool for building an interactive system to verify/find winning strategies for 8×8 or more.
In chapter 5, we conclude the results of this thesis.
目 次
1 序論 1
1.1 Hexのルール . . . . 1
1.2 研究の背景 . . . . 2
1.3 新証明技法の概要 . . . . 5
1.4 検証プログラムの概要 . . . . 6
1.5 本論文の構成 . . . . 7
2 基本概念 8 2.1 仮想連結と仮想準連結 . . . . 9
2.2 ユニオン連結 . . . . 10
2.3 AB-property. . . . 11
2.4 先行排除 . . . . 12
3 新証明技法とその応用 14 3.1 AND-OR連結 . . . . 14
3.2 σ連結とσ拡張 . . . . 16
3.2.1 σ連結 . . . . 17
3.2.2 σ拡張 . . . . 22
3.3 応用 . . . . 25
3.4 第3章のまとめ . . . . 31
4 必勝手順の検証プログラム 34 4.1 プログラムAとプログラムB . . . . 34
4.1.1 仮想連結パターンの利用 . . . . 34
4.1.2 仮想準連結の利用 . . . . 35
4.1.3 探索法 . . . . 36
4.1.4 評価関数 . . . . 36
4.2 必勝手順とその検証 . . . . 36
4.2.1 ゲームの一般的な必勝手順 . . . . 37
4.2.2 Hexにおける必勝手順 . . . . 37
4.2.3 必勝手順の検証方法 . . . . 40
4.3 性能評価実験 . . . . 40
4.3.1 プログラムAの性能評価 . . . . 40
4.3.2 プログラムAとプログラムBの性能比較 . . . . 43
4.4 第4章のまとめ . . . . 46
5 結論 47
謝辞 49
参考文献 51
関連論文 53
著者略歴 54
1 序論
本論文では，ゲームHexの必勝手順の構成法に関して，2つの大きな成果を得た．第 一に，盤面の必勝を導くための新証明技法を提案し，それを応用することで，従来の 方法より簡潔な形で必勝手順を構成することができた（第3章）．第二に，盤面の連結 性を検証するプログラムを提示し，高速な連結判定を実現した（第4章）．
本章の構成は以下の通りである．まず，1.1節でHexのルールを説明する．次に，1.2 節で研究背景を述べる．ここで，必勝手順の構成に関する課題について説明し，今後 の発展において求められていることを明確にする．第3章と第4章の概要について，そ れぞれ1.3節と1.4節で述べる．本論文の構成を1.5節で述べる．
1.1 Hex のルール
ゲームHexは，P. HeinやJ.F. Nashによってルールが考案された完全情報型のゲー ムである．盤面はn×n個の正六角形のセルを菱形に敷き詰めた盤面を用いる．二人の プレイヤは黒石と白石を交互に置いていく（本論文では先手を黒とし後手を白とする）．
先手は上辺と下辺を黒石で，後手は左辺と右辺を白石で連結すると勝利となる．図1 は，先手が勝利している盤面（局面）である．図2は，後手が勝利している盤面（局 面）である．盤面の大きさに規定はないが1 ，実際の対局では，標準的に，10×10や 11×11の盤面が広く用いられる[14]．熟練プレイヤ同士の対局では，14×14∼17×17 の盤面が用いられる場合がある[7]．また，19×19の盤もしばしば用いられる．
ゲームHexは先手が圧倒的に有利である．この先手の優位性を是正するために，実 際の対局では交代ルール（one-move-equalizationrule）を採用している．これは，ゲー ム開始時に一方のプレイヤが初手の（黒）石を置き，他方のプレイヤは，黒石と白石 のどちらの石でそれ以降のゲームをプレイするかを選択できるというルールである．
本論文では左上から順に列と行にそれぞれ 1,2,· · ·, nと番号をふり，セルの位置を 列と行の番号の対で指定する．たとえば，図1の‘♯’で示すセルは62と表す．
# 1
1 2
2
3
3
4
4
5
5
6
6
7
7
図 1: 先手（黒）勝ちの盤面の例
11952年に，P. Brotheresによって販売されたときには，12×12の盤面が用いられていた．
1 1
2
2
3
3
4
4
5
5
6
6
7
7
図 2: 後手（白）勝ちの盤面の例
1.2 研究の背景
ゲームは，コンピュータサイエンスの分野の1つとして，古くから研究されてきた．
ゲームは，ルールが明確で評価がしやすいといった特徴がある．そのため，優れた例 題として古くから用いられており，探索アルゴリズムや人工知能などの研究の発展に 大きく貢献してきた．ゲームの1つのジャンルとして，連結ゲームがある．プレイヤ は，それぞれ自分の石を置いていき，ゲームの勝利条件を目指す．勝利条件は，たと
えばConnect-Fourの場合，自分の石を4個直線に並べることである．他の連結ゲーム
の例として，五目並べ，連珠，Qubicなどが挙げられる[14]．代表的な連結ゲームとし てHexがある．
ゲームHexは，P. Hein（1942年）やJ.F. Nash（1948年）によってゲームのルールが 考案されて以来，今日に至るまで様々な研究が行われてきた．1949年に，J.F. Nashは，
n×nの盤面において先手の必勝手順が存在することを証明した[5, 14]．C. Bergeは，盤 面の解析における基本的な考え方である先行排除（must-play）を導入した[4, 6, 10, 17]． 任意の盤面から勝利プレイヤを求める問題は，1981年にPSPACE-completeであるこ とが証明された[9, 23]．1994年には，B. Endertonが6×6における任意の初手におけ る必勝手順を求めた．2000年代になって，J. Yangら[24, 25]やR. Hayward[10]らが 7×7における必勝手順を求めた．コンピュータプログラムによる世界大会[3, 12]が開 かれているように，対局プログラムに関する研究も盛んに行われてきた．世界初の対 局プログラムは，1953年にC. Shannonらによって作成された．C. Shannonらの対局 プログラムにおける着手の評価法は，近年のQueen-bee[21, 22]やHEXY[1, 2]に応用 されており，これら強力な対局プログラムを実現することに貢献している．このよう に，今日に至るまで多くの研究者達が様々なHexの研究課題に取り組んできた．
ゲームHexは，前述のように，すべてのn×nの盤において，先手必勝手順が存在 することが証明されているが，それを具体的に示すこと（構成的証明）は長年の研究 課題である[14]．Hexは引分けがない．先手が任意の初手を選べるとき先手必勝である が，一般には，初手によっては先手が勝つとは限らない．交代ルールを採用した実際
の対局（competitive Hex）では，盤面のすべての初手に対し必勝であるプレイヤが既
知であれば，黒石か白石の選択権があるプレイヤの勝利する．Hexの必勝手順を求め るという課題に関する研究の流れとして，まず，小さなnにおいて，中心付近の初手
に対する必勝手順が求められる．次に盤面の中心から離れた初手に対して必勝手順が 求められる．その後，より大きな盤面に対する必勝手順が調べられていく．与えられ た盤面から勝利プレイヤを求める問題は，PSPACE-completeであることが証明されて おり，盤面が大きくなると，具体的な必勝手順を示すことは難しくなる．5×5以下で は，人間の熟練プレイヤであれば，任意の局面から勝利プレイヤを求められるとされ
ている[14]．ゲーム木の平均分岐数（branching factor）と終局までの長さは，いずれ
もO(n2)である．8×8以上の盤面では，検証可能な程度に簡潔な形で，必勝手順を扱 うことができないとされてきた[10, 14]．
盤面の大きさが6× 6では，2000年にB. Endertonがコンピュータを用いること ですべての初手における勝利プレイヤを示した[8]．J.Yangら[24]は，decomposition
methodと呼ばれる盤面分割の方法を用いて，7×7（初手44）の必勝手順を示した2 ．
R. Haywardら[10]は，仮想連結による盤面分割に基づくプログラムを作成し，7×7
の初手49種類すべてに対して，いずれのプレイヤが勝利するかを示した．2005年に，
K. Noshita[16, 17]は，ユニオン連結（union-connection）の概念とAB-propertyを導 入し，これに基づき，7×7や8×8に対する完全な必勝手順[18, 19]を示した．
ゲームHexのような二人プレイヤの完全情報型のゲームにおいて，先手（後手）の 必勝手順を示すとは，次のような証明木を書き下すことを意味する：各節点は局面を 示し（根は初期局面を示す），枝は着手を示す．後手（先手）局面に対応する節点は，
あらゆる合法手を枝としていて，子節点はそれらの着手から至る先手（後手）局面を 示す．先手（後手）局面に対応する節点では，正しい着手を示す枝が1つだけあり，そ れにより後手（先手）局面に対応する節点に至る．すべての葉は，先手（後手）の勝 利を実現している局面である3 ．
盤面の大きさが，6×6や7×7以上になると，上記のような証明木を人間の手で示 すことは現実的な方法ではない．コンピュータにより必勝手順を示す（勝利プレイヤ を求める）場合も，（たとえば素朴にAND-OR探索を行うだけでは）計算量という観点 から不可能であると言える．そのため，ゲームHexの必勝手順の構成では，様々な数 学的技法が提案されている．
ゲームHexにおける数学的技法の中で，最もよく知られている方法の1つは，盤面い くつかの領域（セルの集合）に分割し，各々の領域上で必勝（石間の連結）を示す方法 である．たとえば，V.V. Anshelevich[1, 2]は，仮想連結を提案し，これを応用するこ とで強力な対局プログラムを実現した．J. Yangら[24, 25]は，decomposition method と呼ばれる盤面分割の方法により，7×7の必勝手順を示した．K. Noshita[16, 17]は，
ユニオン連結を提案した．ユニオン連結は，仮想連結の概念を一般化し，連結の論理和 を扱えるようにした概念である．ユニオン連結を用いると，仮想連結よりも多くの連結 パターンを扱うことができ，盤面の必勝性を簡潔な形で示すことができる．K. Noshita
2J.Yangは，ホームページで8×8以上の必勝手順を求めたとの記事を載せているが，公式に発表さ
れておらず，詳しい内容は不明である．
3Hexにおける先手（後手）必勝手順では，葉は，黒石（白石）により上辺と下辺（左辺と右辺）が 直接連結している局面を表す．
は，ユニオン連結を必勝手順の証明木における先行排除（局面の枝刈り）に応用する ことで，7×7や8×8の必勝手順を示した．この技法の強力さは，たとえば，7×7
（様々な初手）の必勝手順が（コンピュータを使わないで）容易に検証できることをみ てもわかる．2002年に，H.J. van den Herikは“fundamental breakthrough”無しでは，
8×8以上の必勝手順を扱えないと述べている[14]．R. Rasmussen[20]は，Hexの勝利 プレイヤを求めるアルゴリズムを示したが，（彼のアルゴリズムによると）8×8のすべ ての初手における勝利プレイヤを求めるのは，約9年かかると述べている．今後，大 きな盤面における必勝手順を導いていくためには，より強力な証明技法が必要になっ てくる．
コンピュータを用いた研究では，前述のように，B. EndertonとR. Haywardらが，
それぞれ6×6と7×7の勝利プレイヤを求めた．しかし，実際にコンピュータによっ て完全に自動的に必勝手順を発見することは，7×7でさえ難しい．R. Haywardらは，
アルゴリズムを説明しているが，その詳しい実現方法については述べていない．彼ら のプログラムでは，7×7の必勝手順（すべての初手）を求めるのに約615時間かかっ ている．また，8×8以上の盤面については言及していない．8×8では，盤面の状態 数は，単純計算で，7×7の364−49 ≅ 1.4×107倍となり，コンピュータによって必勝 手順を求めることは不可能とされていた[14] 4 ．実際，7×7の場合でも証明木におけ る探索が複雑になり正しさの検証が難しい．たとえば，J.Yangの7×7の必勝手順[24]
は，2006年になってコンピュータにより正しさが検証された[11]．
このように，必勝手順の発見・検証の両方の側面において，7×7で利用された方法 を8×8以上の盤面で適用していくことは難しい．必勝手順を構成するにあたって，盤 面分割を行うことは必須であるが，コンピュータで適切な盤面分割を行うことは困難 である．そこで，今後さらに大きい盤面における必勝手順を求めていくためには，前 述したように，新しい証明技法の開発はいうまでもないが，人間によって分割された
（部分）盤面における連結性をコンピュータで検証していくなど，人手とコンピュータ の共同作業が必要になってきている．
これまでの述べてきたことからわかるように，ゲームHexの必勝手順の構成におい て，今後さらに大きな盤面における必勝手順を導いていくためには，効率的に必勝手 順を導いていくための証明技法の実現が求められている．さらに，人手とコンピュー タの共同作業で必勝手順を導いていくシステムを実現する必要がある．前者を実現す るものとして，第3章では，互いに重複した領域における盤面分割を扱う証明技法を 提案する．本論文の証明技法を用いることで，既存の手法（仮想連結やユニオン連結 など）に比べて，より多様な盤面分割のパターンを扱えるようになる．これにより，従 来の方法だけでは複雑すぎるとされてきた盤面に対し，非常に簡潔な形で必勝手順を 構成できる．後者を実現するものとして，第4章では，高速に局面のユニオン連結性
4本論文の関連論文[1]（参考文献[28]（2008年12月））と関連論文[2]（参考文献[29]（2009年2月））
の発表後の2009年6月に，P. Hendersonら[13]が8×8の勝利プレイヤを求めた（Proc. 21st IJCAI）．
著者らは，参考文献[27]（2006年11月）にて，関連論文[2]の基本的なアイデアについて述べた．P.
Hendersonらは，参考文献[13]において，著者らが参考文献[27]で提示した必勝手順（8×8（初手63））
で現れる特に重要な2つの局面の正しさを検証した．
を判定するプログラムを作成し，評価実験を行った．次の1.3節と1.4節では，それぞ れ第3章と第4章の概要について述べる．
1.3 新証明技法の概要
前節で述べたように，効率的に必勝手順を求めていくための証明技法の開発が望ま れている．そこで，本論文では，互いに重複する領域において盤面分割を行う新証明 技法を提示する．第3章では，σ連結の概念とσ拡張の技法を提案し，これらを必勝 手順の構成に応用する．そのために，まず，AND-OR連結を定義する．AND-OR連結 は，領域（空セルの集合）における連結の論理和・論理積を扱うものである．σ連結は，
AND-OR連結における領域内の着手指定を表現するものである．σ拡張は，その領域
の外部の特定のセルに先手が着手することにより，より大きい領域に対するAND-OR 連結に拡張する技法である．σ連結の領域内の石の配置は，着手指定により，有限の パターンに分類される．よって，簡単な場合分けを行うことにより，σ拡張で新たに
AND-OR連結を得られることを証明できる．
本論文のσ連結とσ拡張を用いると，従来の方法よりも多様な盤面分割のパターン を扱えるようになり，複雑な盤面でも容易に必勝を示せる．既存の方法では，後手の すべての候補手に対して，必勝となる先手の着手を発見する必要があった．σ連結を盤 面に適用すると，その領域内への後手の着手は，先手の応手が予め指定されているた め，考慮する必要がない．σ連結の領域と，その外部の領域を連接するときには，σ拡 張によって得られるAND-OR連結を利用する．
第3章の目的は，σ連結とσ拡張を用いることで，新たな証明法を確立し，先手勝ち の証明に応用することである．本論文で提案するσ連結より，空セルの集合内の着手 手順を予め定めることができる．これを利用し，σ連結とσ拡張を応用して必勝を求 めるとき，探索はその領域の外に対して行う．過去に示されている必勝手順では盤面 全体を探索していたのに対し，本論文の方法ではσ連結の着手指定の証明木（部分木）
とそれ以外の領域の探索によって先手勝ちを証明する．結果として，盤面全体を探索 する手間を省き，複雑な解析が必要な盤面を大幅に減らすことができる．それにより，
従来の方法では複雑すぎるとされていた盤面に対して完全な形で必勝手順を記述でき るようになる．
新技法の強力さを示す応用例として，8×8の盤面を取り上げ，先手勝ちを示す．従 来の方法のみでは，その局面から派生するすべての子節点について探索を行わなけれ ばならない．σ連結とσ拡張を用いることで，盤面全体に対して探索を行う必要がな くなる．探索範囲が減少することで解析（先行排除）が容易になり，深い探索が必要 なくなる（自明な強制着手が得られる）．
さらに，σ連結とσ拡張を最大限に利用すれば，8×8（初手54）の先手必勝手順を 従来より簡潔な形で示すことができる．ほとんどの後手の着手は，σ連結とσ拡張を 適用することにより，深い探索をせずに先手勝ちを求められる．そのような後手の着 手を除外すると，8×8（初手54）の必勝手順は総節点数13個の証明木で表すことが できる．そのうち，先手局面は6個であり，後手局面は7個である．必勝手順を示すた
めに基本となるσ連結とσ拡張の数はそれぞれ4個である．バリエーションを含める と，6個のσ連結と6個のσ拡張が必要になる．この必勝手順を完全な形で証明するに あたって，必要な解析図の総数は99個である．このように，従来の必勝手順（たとえ ば参考文献[19]）に比較して簡単に必勝手順を記述できるようになる．
1.4 検証プログラムの概要
前節で述べたように，今後さらに大きな盤面における必勝手順を構築していくため には，人間とコンピュータの共同作業が重要となってきている．特に，人の手によって 分割された盤面に対して，コンピュータにより盤面の連結性を証明することは不可欠 である．また，この部分は，計算量という点において大きな部分を占める．そこで，第 4章では，ユニオン連結の成否を出力する連結判定のプログラム（プログラムAとプロ
グラムB）を作成した．さらに，プログラムAとプログラムBの性能を評価するため，
K. Noshita[16, 17]の示した必勝手順におけるユニオン連結の正しさの検証を行った．
プログラムAとプログラムBの基本的なアルゴリズムは，ハッシュ表を用いたAND- OR探索であるが，Hex特有の手法を取り入れることによって，探索の高速化を図って いる．プログラムA，プログラムB共に，着手の順序付けのために，Hexに依存した 多くの評価項目を線型結合した評価関数を用いている．各々の探索節点では，着手候 補を限定する手法（先行排除）を用いることによって，探索を行う必要のない着手を取 り除いている．また，基本的な仮想連結の連結パターンを登録して，パターンの照合 により，探索の能率向上を図っている．さらに，プログラムBでは，仮想準連結[1, 2]
に基づく連結判定法を組込んでいる．
プログラムAの有用性を評価するため，実例として，K. Noshitaの示した7×7 の 必勝手順の正しさの検証を行った．K. Noshitaの示した証明木の（後手局面の）節点 には，ユニオン連結に基づいて分割された盤面が付与されている．これらの分割され た部分盤面を入力として与えた．その結果，すべてのユニオン連結においてその正し さを確かめることができた．入力として与えたユニオン連結の総数は23個であるが，
1分以下の計算時間で全ての検証を行うことができた．
次にプログラムAとプログラムBの性能比較を行う．そのために，K. Noshitaの示 した8×8の盤面における必勝手順で，主要なユニオン連結の正しさを検証した．プロ グラムBの方がプログラムAに比べて，概ね短い実行時間で検証を終了している．実 行時間の差が顕著に現れたものでは，200倍近い差が現れたものがあった．
計算時間について，本論文のプログラムは，必勝手順の検証・発見の実用に足ると 判断できる．また，着手の順序付けと先行排除ともに，人間の熟練者と同じ程度に正 確に行っている．
第4章における貢献は，人間とコンピュータの共同作業によって必勝手順を導いて いけることを，具体的な実験データをもって示したことである．特に，8×8以上の必 勝手順を検証するための最も基本的な道具で，実用性能をもつものを実現したことは，
大きい貢献であるといえる．プログラムAとプログラムBの性能評価実験では，7×7 と8×8の盤面において，プログラムAとプログラムB共に連結性を証明するために
充分実用的な早さで検証を終えている．これらの実験結果は，人間とコンピュータの 共同作業により 8×8以上の必勝手順を導くためのシステムが実現可能であることを 示しているといえる．
1.5 本論文の構成
本論文の構成を以下で述べる．第2章では，既存研究における基本的な概念につい て述べる．本論文で用いる用語や記号の定義を行い，後の章で用いる補題を示す．第 3章で，必勝手順を導くための概念としてσ連結を定義し，それに基づく技法であるσ 拡張について述べる．これらを用いることで，簡単に必勝の証明を得られることを具 体例を挙げて示す．応用として，本論文の証明法に基づき，従来の方法より簡潔な形 で必勝手順を構築できることを示す．第4章で，本論文で作成した必勝手順の検証プ ログラムについて述べる．K. Noshitaの必勝手順[16, 17]を取りあげ，プログラムの性 能評価実験を行い，それらの実験結果を示す．第5章で，本論文の総括を行う．
2 基本概念
本章では，既存研究における基本的な概念について説明する．本論文で用いる用語 や記号の定義を行い，いくつかの補題を示す．なお，本章で示す補題は，本論文中で 特に明記することなく使用する場合がある．
本論文では，プレイヤP（先手か後手）に対し，∼ P をP でないプレイヤとする．
盤面の一部のことを部分局面という．以下では，特に区別する必要がないとき，ある いは文脈から明らかなとき，部分局面を単に局面ということがある．先手の石とは黒 石を示し，後手の石とは白石を示す．プレイヤP の手番である（部分）局面をP の局 面，あるいはP 局面と呼ぶ．
ある石と，それに直接連結する同色の石からなる石の集合を群と呼ぶ．セルxに置 かれた石を含む群をxと書く．黒石からなる群を黒の群，あるいは先手の群という．白 石からなる群を白の群，あるいは後手の群という．
セルcに石が置かれていないとき，cは空セルであるという．セルの集合Sに対しセ ルc ∈ SをS上のセルという．すべてのc ∈ Sが空セルであるとき，Sを空セルの集 合という．セルの集合Sに対し，S上のすべての空セルからなるセルの集合をe(S)と する．
前述（1.1節）したように，盤上のセルを列と行の番号の対で表す．
以下では，n×nの盤面において，次のような黒の群tとb，白の群lとrを仮定す る（図3）．
盤面に10, 20,· · ·, n0, 1(n+ 1), 2(n+ 1),· · ·, n(n+ 1)のセルが存在すると仮定し，
それらのセルに黒石が置かれているものとする．tを10, 20, · · ·, n0のセルに置かれた 石からなる黒の群とする．bを1(n+ 1), 2(n+ 1), · · ·, n(n+ 1)のセルに置かれた石 からなる黒の群とする．盤面で黒石がtとbを連結するとき，その盤面は先手勝ちで ある．
盤面に01, 02, · · ·, 0n, (n+ 1)1, (n+ 1)2, · · ·, (n+ 1)nのセルが存在すると仮定し，
それらのセルに白石が置かれているものとする．lを01, 02, · · ·,0nのセルに置かれた 石からなる白の群とする．rを(n+ 1)1,(n+ 1)2,· · ·, (n+ 1)nのセルに置かれた石か らなる白の群とする．盤面で白石がlとrを連結するとき，その盤面は後手勝ちである．
t
b
l r
図 3: n×nの盤面
2.1 仮想連結と仮想準連結
本節では，V.V. Anshelevichが提案した仮想連結[1, 2]について説明する．
Sを空セルの集合とし，aとbをP の群とする．先手と後手の着手をSのセルに限 定すると仮定する．仮想連結S[ab]とは，∼P から着手をはじめても，P の石がaとb を連結することができる．
以下では，仮想連結S[ab]において，図や文脈よりSが明らかであるときは，a−b と書く．
φを，任意のセルの集合Sに対し，φ⊆Sを満たす空セルの集合とする．φ∩S=φ, φ∪S =Sと約束する．また，任意の群aに対し，φ[aa]と約束する．同色の群xとy が直接連結するとき，φ[xy]と書く．
図4において，x, y, z,uをそれぞれ32, 24, 52, 46のセルとする．この図では，代表 的な仮想連結の例を3つ挙げている．これらの例は，Skip Lemma（S-lemma）と呼ば れる仮想連結とTrapezoid Lemma（T-lemma）と呼ばれる仮想連結である[16, 17]．
次の補題1と補題2で，S-lemmaとT-lemmaを示す．
補題 1 （S-lemma）S（S’）を図4の23と33（51と61）の2個の空セルからなる 集合とする．このとき，S[tx]（S′[tz]，それぞれ）が成り立つ．
補題 2 （T-lemma）T を図4の‘∗ ’で示す8個のセルからなる集合とする．このと き，T[ub]が成り立つ．
+ +
x z
+ + y
u *
* * *
* * * *
1 1
2
2
3
3
4
4
5
5
6
6
7
7
8
8
図 4: 仮想連結の例
V.V. Anshelevichは仮想連結だけでなく，次で示す仮想準連結[1, 2]について述べて いる．
T をセルの集合とし，cとdをP の群とする．先手と後手の着手をT に限定すると 仮定する．仮想準連結T |cd|とは，P から着手をはじめたとき，P の石がcとdを連 結することができる．
仮想連結と仮想準連結の変換規則を次の（i）と（ii）で示す[1, 2]．（i）と（ii）に おいて，Si(1≤i≤k)は空セルの集合を表す．
（i）S1∩S2 =φ, S =S1∪S2のとき，S1[ab]かつS2[bc]ならばS[ac].
（ii）∩ki=1Si =φ, S =∪ki=1Si, k > 1のとき，すべてのi (1 ≤ i ≤ k)に対しSi | ab| ならばS[ab].
2.2 ユニオン連結
本節では，K. Noshitaが提案したユニオン連結[16, 17]について説明する．
Sを空セルの集合とし，a1, a2,· · ·, ak, b1, b2,· · ·,bkをP の群とする．先手と後手の 着手をSに限定すると仮定する．ユニオン連結S[a1b1 ∨a2b2∨ · · · ∨akbk] とは，∼P から着手をはじめても，あるi(1≤i≤k)が存在しP の石がaiとbiを連結することが できる．
k = 1のとき，ユニオン連結は仮想連結である．
仮想連結と同様に，ユニオン連結も図や文脈よりSが明らかであるときは，a1−b1∨ a2−b2∨ · · · ∨ak−bkと書く．
図5において，x, y,z, wをそれぞれ黒石の置かれた34, 62, 54, 46のセルとする．こ の図では，ユニオン連結の例を2つ示している（補題3と補題4）．
- - - - -
- - - - - y
- - - -
- x * z
* *
* * w
* *
* 1
1 2
2
3
3
4
4
5
5
6
6
7
7
8
8
図 5: ユニオン連結の例
補題 3 V を図5の‘-’で示す15個の空セルからなる集合とする．このとき，V[tx∨yx]
が成り立つ．
補題 4 Wを図5の‘∗’で示す8個の空セルからなる集合とする．このとき，W[xz∨ xw∨xb]が成り立つ．
補題3では，V における後手の第一着手（Vが空セルの集合の場合における着手）が，
41, 51, 42, 33, 43以外のセルに行なわれたとき，先手は42のセルに着手する．このと
き，S-lemmaよりx−t．41, 51, 42, 33, 43の5つのセルに対する着手のうち，白41に 対して黒42，白33に対して黒43，他の3つに対して黒23を着手すると，それぞれの 局面でe(V)[tx∨yx]が成り立つ．
補題4では，Wにおける後手の第一着手が44以外のセルに行なわれたとき，先手は 44に着手する．このとき，xとzが連結する．白44に対し，先手は黒26を着手する．
このとき，S-lemmaより，x−26が成り立つ．次の後手の着手がセル36へ行なわれた とき，先手（黒）は18に着手する（36以外のセルへの着手に対しては黒36を着手す る）．このとき，S-lemmaより26−bが成り立つ．よって，x−bが成り立つ．
ユニオン連結の変換規則を次の（1）と（2）で示す[16, 17]．
η=a1b1∨a2b2∨ · · · ∨akbk(k≥1)とすると，次の（1）と（2）が成り立つ．
（1）S[ab∨ab∨η]ならば S[ab∨η].
（2）S1∩S2 =φ, S =S1∪S2のとき，S1[ab∨η]かつS2[bc∨η] ならばS[ac∨η].
ユニオン連結の変換規則は（１）と（２）以外にも存在する．このことは文献[16, 17]
で述べられている．
ここで，空セルの集合SとP の群a1, a2, · · ·, ak, b1, b2, · · ·, bkに対し，次のように S |a1b1∨a2b2 ∨ · · · ∨akbk| を定義する．
先手と後手の着手をSに限定すると仮定する．S |a1b1∨a2b2∨ · · · ∨akbk| とは，P から着手をはじめたとき，あるi(1≤i≤k)が存在しP の石がaiとbiを連結すること ができる．
盤面分割の方法（たとえば仮想連結やユニオン連結に基づく必勝の証明方法）は，
ゲーム木探索で生じる場合分けの簡単化のために古くから用いられている．ユニオン 連結を用いると，仮想連結に比べて，より一般的な連結のパターンが扱えるようにな る．これにより，ゲーム木の探索の場合分けの数が小さくなり，簡潔な形で必勝手順 を示せる．たとえば，7×7（初手44）の必勝手順を，（仮想連結に基いた）J. Yang[24]
の証明に比べて，少ない図面の数で記述できる[16, 17]．このように，より広範囲で連 結のパターンを扱う方法を考案することは，必勝の証明を簡単に記述するために（大 きな盤面において必勝手順を示すために）重要である．
2.3 AB-property
本節では，K. NoshitaのAB-propertyについて説明する[16, 17]．
空セルの集合をSとし，A, B(∈ S, A ̸= B)を空セルとする．a1, a2, · · ·, ak, b1, b2,
· · ·,bk をP の群とする．先手と後手の着手をSに限定すると仮定する．ユニオン連結 S[a1b1∨a2b2∨ · · · ∨akbk]に関するAB-propertyとは，∼P から着手をはじめても，す べての∼P 局面において次を成り立たせることができる：セルAに∼P の石が置かれ ているとき，セルBにP の石が置かれていて，かつ，e(S)[a1b1∨a2b2∨ · · · ∨akbk]で ある．セルBに∼P の石が置かれているとき，(e(S)− {A})[a1b1∨a2b2∨ · · · ∨akbk] である．それ以外のときe(S)[a1b1∨a2b2∨ · · · ∨akbk]である．
具体例を図6で示す．xを33のセルとしT を‘∗ ’, A, Bで示す8個の空セルからな る集合とする．この図は，ユニオン連結T[tx]（T-lemma）に関するAB-property（参 考文献[17]のLemma 3）を示している．
K. Noshitaの8×8の必勝手順における証明の文書において，先手必勝を表すいくつ
かの盤面では，ユニオン連結に加え，このAB-propertyを導入することで先手勝ちを
示している．AB-propertyは，2つの領域が部分的に重複している場合においても，そ こで成り立つ連結を扱うことができる．第3章で提案する新証明技法は，重複する領 域（セルの集合）における連結を広範囲で扱えるようにしたものである．
* * * A
* * B
1 1
2
2
3
3
4
4
5
5
6
6
7
7
* x
図 6: AB-propertyの例
2.4 先行排除
先行排除（must-playと呼ばれることもある）の考え方は，様々なゲームにおいて古 くから知られている[4, 6, 10, 17]．
Bを与えられた局面とする．Sを空セルの集合としx1, x2, · · ·, xk, y1, y2, · · ·, ykを P の群とする．局面BのS上の空セルcにP の石を置いた局面において，ある空セル の集合T ⊆Sが存在し，T[x1y1∨x2y2∨ · · · ∨xkyk]が成立すると仮定する．このとき，
局面Bにおいて，(T ∪ {c})|x1y1∨x2y2∨ · · · ∨xkyk|が成立する．
この性質は次のことに用いられる．∼P の局面においてP の石を置いた局面を調べ ることで∼P の悪い着手の集合を求め，それら悪い着手を局面の着手候補から取り除 く．このようにして，着手候補を取り除くことを先行排除という．
1 1
2
2
3
3
4
4
5
5
6
6
7
7
図 7: 後手局面
後手局面における先行排除を例に説明する．図7は後手の局面であるが，この局面 で先手の石を1つ置き，ある空セルの集合Sに対しS[tb] である（先手が勝利できる）
場合を考える．
セル52に黒石を置いたとき（図8），図の色の付いた空セルからなる集合をM1とす ると，(M1− {52})[tb]である．このことは，後手が（図7の局面において）M1に含ま
れないセルに着手すると，次に先手が黒52を着手することで先手勝ちとなることを意 味する．
同様に，セル36に黒石を置いたとき（図9），図の色の付いた空セルからなる集合 をM2とすると，(M2− {36})[tb]である．このことは，後手が（図7の局面において）
M2に含まれないセルに着手すると，次に先手が黒36を着手することで先手勝ちとな ることを意味する．
図10において，M1∩M2を色の付いた8個のセルで表す．図7の盤面では，これら 8個のセル以外に対する後手の着手に対し，次に先手は黒52か黒36を着手することで 先手勝ちとなる．
+ + + +
*
* * *
* * * *
1 1
2
2
3
3
4
4
5
5
6
6
7
7
図 8: 先行排除の例1
. . . . . .
. . . . .
. . . .
. . . .
. .
. + +
1 1
2
2
3
3
4
4
5
5
6
6
7
7
図 9: 先行排除の例2
1 1
2
2
3
3
4
4
5
5
6
6
7
7
図 10: 先行排除により残った後手の着手
3 新証明技法とその応用
本章では，盤面の連結性を表す新しい概念としてσ連結を定義し，それに基づく技 法であるσ拡張について述べる．本章の目的は，これらを用いて新しい必勝の証明方 法を確立し，必勝手順の構成に応用することである．
本章のσ連結とσ拡張は，互いに重複している2つの領域に対し，盤面の連結を扱 えるようにするものである．σ連結の特徴は，領域の全ての後手の着手に対し先手の 応手を指定することにある．σ拡張は，σ連結が成り立つ領域の外部の特定のセルに着 手することにより，より大きい領域に対する連結を得る技法である．本章のσ連結と σ拡張を用いると，従来の方法に比べ簡潔な形で必勝を証明することができる．σ連結 による着手指定により，その領域内に対する着手は探索時に考慮する必要がない．σ連 結の領域と，その外部の領域を連接する際には，σ拡張を用いて連結を得る．これら に基づき，従来の方法だけでは，必勝を示すのが複雑すぎるとされてきた局面に対し，
簡潔な形で必勝を証明できるようになる．σ連結とσ拡張の応用して，8×8（初手54）
の必勝手順を構成する．
本章の構成について説明する．まず，3.1節では，AND-OR連結を定義する．これに より，連結の論理和・論理積，それらの複合を扱えるようにする．次の3.2節では，σ 連結とσ拡張について述べる．ここでは，最初にσ連結を定義し，その具体例を用い て説明を行う（3.2.1節）．その後，3.2.1節で述べたσ連結の例に基づき，σ拡張を適 用し，重複した領域上で連結が得られることを示す（3.2.2節）．新証明技法の応用を 3.3節で述べる．ここでは，σ連結とσ拡張を用いた必勝の証明方法について，具体例 を用いて述べ，実際に必勝手順を構築する．本章のまとめを3.4節で行う．
なお，本章では，先手（黒）の必勝手順を求めるための証明法を提案しているが，手 法自体は後手勝ちを示すことにも用いることができる．一般的には，先手・後手に関 わらず，（存在するのであれば）必勝手順を求めることに応用できる．たとえば，「先手 が初手に悪手を着手した後の局面における後手の必勝手順」を求めるために応用でき る．先手・後手のどちらのプレイヤにおいても，「必勝手順を求める」という課題に対 して，問題の一般性は損われない．
3.1 AND-OR 連結
P の群x, yに対し，xyをP に関するリテラルといい，xとyが連結していることを 表す．
ここで，P に関するAND-OR式を次のように定義する．
• P に関するリテラルはP に関するAND-OR式である．
• P に関するAND-OR式α,βに対し，α∧βはP に関するAND-OR式である．
• P に関するAND-OR式α,βに対し，α∨βはP に関するAND-OR式である．
次のような根付きラベル木を準ゲーム木という．
1. 根には∼P の部分局面が関連付けられている．
2. 根以外の節点には部分局面と着手が関連付けられている．
3. 根以外の深さが偶数（奇数）の節点にはP（∼P，それぞれ）の着手が関連付け られている．
4. 深さ奇数の節点は1つの子をもつ．
根以外の節点に関連する部分局面は，根に関連する部分局面に対し根からその節点に 至る経路上の（節点に関連する）着手を順に行なって得られるものとする．P（∼P）の 部分局面が関連付けられている節点をP 節点（∼ P 節点），あるいはP の節点（∼ P の節点，それぞれ）という．
部分局面Bに対し，次のような準ゲーム木を準必勝木という．
1. 根にはBが関連付けられている．
2. 葉以外の深さ偶数の節点は，関連する部分局面におけるすべての着手を子とする．
定義 5 （AND-OR連結）∼P の部分局面をBとし，Bのすべての空セルからなる
セルの集合をSとする．P に関するAND-OR式をαとする．AND-OR連結S[α]と は，Bに対し準必勝木T が存在し，T のすべての葉においてαが成立することである．
特に明記しない場合，AND-OR式は先手に関するAND-OR式とする．
本論文では，一般の論理式における（否定を含まない）和積標準形と積和標準形に
相当するAND-OR式のみを用いる．前者の形をしたAND-OR式を和積形，後者の形
をしたAND-OR式を積和形という．一般のAND-OR式に対し，それと論理的に等価
な和積形・積和形のAND-OR式が存在する．
AND-OR連結に関係するいくつかの性質を次で示す．これらは簡単に証明すること
ができる．
次の（1）∼（3）において，∼P の部分局面をBとし，Bのすべての空セルからな るセルの集合をSとする．空セルの集合S1,S2に対し，S1∩S2 =φ,S =S1∪S2と仮 定する．
（1）x, y, z, wをP の群とする．α1, α2, α3, β1, β2, β3をP に関するAND-OR式とす る．α1,α2,α3は和積形，β1, β2,β3は積和形であると仮定する．このとき，以下が成 立する．
（1-1）S1[α1]かつS2[α2]ならS[α1∧α2].
（1-2）任意の局面においてxy∧zwならxyが成立する．
（1-3）任意の局面においてxyならxy∨zwが成立する．
（1-4）任意の局面においてxy∨xyならxyが成立する5 ．
5（1-4）は冪等律に相当する性質を示す．この性質の他に，吸収律，分配律，交換律，結合律などに 相当する性質が成り立つ．
（1-5）任意の局面においてxy∧yzならxy∧yz∧xzが成立する．
（1-6）S[α1∧α3]とする．すなわち，Bに対し準必勝木T が存在し，T のすべての 葉においてα1 ∧α3が成立する．いま，T のすべての葉においてα1ならα2と仮定 する．このとき，S[α2∧α3]が成立する6 ．
（1-7）S[β1∨β3]とする．すなわち，Bに対し準必勝木T が存在し，T のすべての葉 においてβ1 ∨β3 が成立する．いま，T のすべての葉においてβ1ならβ2と仮定す る．このとき，S[β2∨β3]が成立する.
（2）x, y, xi, yi (1≤i≤p), zj, wj (1≤ j ≤ q)をP の群とする．このとき，以下が成 立する．
（2-1）S[(∨pi=1xiyi)∧(∨qj=1zjwj)]ならS[∨pi=1(∨qj=1xiyi∧zjwj)].
（2-2）S[∨pi=1(xy∧xiyi)]ならS[xy∧(∨pi=1xiyi)].
（3）xi, yi (1≤i≤p),zj, wj (1≤j ≤q)をP の群とする．このとき，S1[∧pi=1xiyi]か つS2[∨qj=1zjwj]ならS[∨qj=1(∧pi=1xiyi∧zjwj)].
補題 6 図5（2.2節）において，V を‘ ∗ ’で示す15個の空セルからなる集合とし W を‘ - ’で示す8個の空セルからなる集合とする．Z = V ∪W とする．このとき，
Z[tz∨tw∨tb∨yz∨yw∨yb]が成立する．
証明 補題3と補題4より，V[tx∨yx]かつW[xz∨xw∨xb]である．また，V ∩W =φ である．
よって，Z[(tx∨yx)∧(xz∨xw∨xb)].（（1-1）より）
Z[(tx∧xz)∨(tx∧xw)∨(tx∧xb)∨(yx∧xz)∨(yx∧xw)∨(yx∧xb)].（（2）より）
Z[(tx∧xz∧tz)∨(tx∧xw∧tw)∨(tx∧xb∧tb)∨(yx∧xz∧yz)∨(yx∧xw∧yw)∨ (yx∧xb∧yb)].（（1-5）と（1-7）より）
Z[tz∨tw∨tb∨yz∨yw∨yb].（（1-2）と（1-7）より）
以上より，補題6が成立する．
3.2 σ 連結と σ 拡張
本節では，σ連結とσ拡張について説明する．まず，3.2.1節でσ連結を定義し，そ の具体例を用いて説明を行う．次に，3.2.2節でσ拡張について説明を行う．ここでは，
3.2.1節で提示するσ連結を用いてσ拡張を示す定理の証明を行う．これらの応用を3.3
節で述べる．
6（1-6）と（1-7）の性質は，一般的には次のことを意味する（AND-OR式の単調性を利用すること でこのことを示せる）．
Pに関するAND-OR式をζ,θとし，（Pに関する）AND-OR式λに現れるζをθに置き換えたAND- OR式をµとする．S[λ]が成立し，それに関する準必勝木のすべての葉においてζならθが成立すると き，S[µ]が成立する．
このことは（和積形でも積和形でもない）一般のAND-OR式に対しても成立する．
![図 30: 9 × 9 （初手 55 ）の証明木（参考文献 [27] の証明木を改訂）](https://thumb-ap.123doks.com/thumbv2/123deta/7735559.1711793/42.892.202.703.79.1021/図39×9初手55の証明木参考文献27の証明木を改訂.webp)
