包括的グレブナ一基底系を利用した限量子消去

摘要

Weispfenningはグレブナ一基底の性質を利用して,包括的グレブナ一基底(comprehensive Gr?bner basis,以下CGBと略記する,[14]参照)による限量子消去(quantifier elimination,以下QEと略記する)アルゴリズムを提案した([15]参照).このQEアルゴリズムは等式制約が多い場合には非常に有効なアルゴリズムであり,束縛変数について等式制約が零次元イデアルとなるような場合には非常に高速なQEが可能となる.近年になりCGB及びその計算に必要な包括的グレブナ一基底系(comprehensive Gr?bner system,以下CGSと略記する)計算に関する効率的なアルゴリズム([4,5, 6,7,8,9,10,11, 13])が提案されている.こうした背景から現在のCGS計算アルゴリズムを利用し,さらにWeispfenningのQEアルゴリズムを改良したアルゴリズムを構築して,高速なQEに実装を行うことを目標とした.