代数的仕様の実現検証において、実現の正しさとは与えられた仕様と実現を記述 した仕様（実現仕様）が振舞的に区別がつかないときとされる。この振舞的な正 しさの関係は振舞実現関係といわれる。
振舞実現関係を検証するためには、与えられた仕様の各公理の両辺が実現仕様の もとで振舞的に等価であることを証明すれば十分である。２つの式が振舞的に等 価であるというのは観測可能な結果を返すすべてのテストによってそれらを区別 できないことをいう。したがって振舞等価性を証明するためには、あらゆる観測 可能な文脈で表される、すべてのテストに対して等価性を調べる必要がある。し かし、無限に存在する観測可能な文脈すべてについて等価性を調べることは、一 般には容易ではない。
この振舞等価性を検証する手法の１つにCoinduction法がある。この手法は、隠 蔽合同という概念を用いることによって、振舞等価性を間接的に扱い検証をしや すくしている。しかし、隠蔽合同を発見するのは、人の力によるところが大きく 自動化が難しい。
そこで、振舞等価性を検証する手法として線形文脈帰納法が提案されている。線 形文脈帰納法は、線形文脈という限られた形の文脈に対して等価性を調べること により、振舞等価性を検証するという手法である。線形文脈とは、文脈の根から 穴までの経路以外はすべて変数であるような文脈である。このような文脈の根か ら穴までの長さに関する帰納法が線形文脈帰納法である。そして、振舞等価性証 明には、線形文脈帰納法を用いて証明すれば十分であることが示されている。ま た、検証法として文脈の長さに関する素朴な帰納法を用いているため、自動化し やすいと考えられている。
本研究では、線形文脈帰納法において文脈の根から穴までの経路以外はすべて変 数であるという定義が証明段階で適用できる公理の形を制限している点に着目 し、線形文脈帰納法の拡張について考える。具体的には、文脈の根から穴までの 経路以外は高々１つの関数記号を含む深さ１以下の項であるような文脈を巾２の 線形文脈として定義し、この新たに定義された線形文脈の根から穴までの長さに 関する帰納法を提案する。そして、振舞等価性証明には巾２の線形文脈帰納法を 用いて証明すれば十分であることを証明する。また、例を用いて従来の線形文脈 帰納法との比較を行いながら、巾２の線形文脈帰納法を用いた検証法の有効性に ついて考察する。